In Haskell, how to explictly give a signature to this particular subfunction with inherited parameters?

Question

Say you have this function

import Control.Monad
import Control.Monad.ST
import Data.STRef

f :: (Num a, Ord a) => STRef s a -> ST s ()
f i = loop
        where
            loop = do
                _i <- readSTRef i
                writeSTRef i (_i - 1)
                when (_i > 1) loop

in loop's body, i is implictly defined as it is a parameter from f. However I'm having a trouble giving a signature to loop. Hie shows me that it should be ST s (), so I write loop :: ST s () just above loop's definition.

However ghc complains that it cannot match the s from loop with the s from f. As loop has no parameter it creates its own local forall s. in that loop's definition which prevents matching with f's s.

But surprisingly it compiles without explicit signature. PartialTypeSignature works but it's ugly and doesnt allow reference to s. It also compiles if I just add i as parameter to loop but let's say I'm lazy.

How can I exlicitly specify loop's signature in a way that compiles?

Is it not true that everything that compiles with implicit types, can be given explicit types so that it still compiles?

Answer 1

The solution does indeed lie in -XScopedTypeVariables

The issue comes from the fact that if you want to refer to an already existing type variable, that variable must be explicitly quantified.

{-# LANGUAGE ScopedTypeVariables #-}
import Control.Monad
import Control.Monad.ST
import Data.STRef

f :: forall s a. (Num a, Ord a) => STRef s a -> ST s ()
f i = loop
        where
            loop :: ST s ()
            loop = do
                _i <- readSTRef i
                writeSTRef i (_i - 1)
                when (_i > 1) loop