[Haskell-cafe] Applying typed hole proposal leads to compilation failure
mniip
14 at mniip.com
Fri Aug 24 21:36:56 UTC 2018
> • Found type wildcard ‘_c’ standing for ‘c’
> Where: ‘c’ is a rigid type variable bound by
> the type signature for:
> f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
> at Test.hs:15:1-32
Emphasis on "rigid". It's not telling you to introduce a new type
variable and put that there. It's telling you that the type you need to
put there is an existing type variable's type.
When you write 'run :: MS c Int a -> (Either String a, Int)' you
implicitly mean 'run :: forall c.' which is exactly introducing a new
type variable.
> • Couldn't match type ‘c1’ with ‘c’
> ‘c1’ is a rigid type variable bound by
> the type signature for:
> run :: forall c1 a. MS c1 Int a -> (Either String a, Int)
This is the 'c' you bound with the implicit 'forall'. The compiler is
asked to verify that 'run' indeed works 'forall c1', so during
typechecking of the function body the 'c1' variable is also rigid.
> ‘c’ is a rigid type variable bound by
> the type signature for:
> f1 :: forall (m :: * -> *) c. MonadIO m => c -> m Bool
This is the 'c' from the typed hole suggestion up above, still rigid.
A part of the typechecking algorithm is that two rigid type variables
cannot be equated.
The solution *actually* proposed by GHC in the wildcard suggestion is to
use the 'c' variable from 'f1's type for which you need to make it
scoped with an explicit 'forall':
f1 :: forall c. (MonadIO m) => c -> m ()
f1 c = do
let _x1 = run f2
let _x2 = run f3
return ()
where
run :: MS c Int a -> (Either String a, Int)
run = runMS c 0
f2 :: MS c s Bool
f2 = pure False
f3 :: MS c s [Int]
f3 = pure []
More information about the Haskell-Cafe
mailing list