<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Hello Cafe,</p>
<p>I encountered a strange issue regarding typed hole. If I ask GHC
(8.4.3) for a typed hole proposal, it says 'use c', but if I use
'c', it complains that it can't unify 'c' and 'c1'.</p>
Why does GHC think those two are different and how to tell to GHC
they are the same?
<p><br>
</p>
Best regards,
<p>vlatko<br>
</p>
<p><br>
</p>
<p><b>Typed hole proposal:</b><br>
• Found type wildcard ‘_c’ standing for ‘c’<br>
Where: ‘c’ is a rigid type variable bound by<br>
the type signature for:<br>
f1 :: forall (m :: * -> *) c. MonadIO m => c
-> m Bool<br>
at Test.hs:15:1-32<br>
• In the type signature:<br>
run :: MS _c Int a -> (Either String a, Int)<br>
<br>
<b>Error when typed hole used:</b><br>
• Couldn't match type ‘c1’ with ‘c’<br>
‘c1’ is a rigid type variable bound by<br>
the type signature for:<br>
run :: forall c1 a. MS c1 Int a -> (Either String a,
Int)<br>
at Test.hs:21:5-47<br>
‘c’ is a rigid type variable bound by<br>
the type signature for:<br>
f1 :: forall (m :: * -> *) c. MonadIO m => c -> m
Bool<br>
at Test.hs:15:1-32<br>
Expected type: MS c1 Int a -> (Either String a, Int)<br>
Actual type: MS c Int a -> (Either String a, Int)</p>
<p><b><br>
</b></p>
<p><b>Minimal runnable example:</b><br>
</p>
<p><font size="-1"><tt>{-# LANGUAGE ScopedTypeVariables,
PartialTypeSignatures #-}</tt><tt><br>
</tt><tt>module Test where</tt><tt><br>
</tt><tt><br>
</tt><tt>import Prelude</tt><tt><br>
</tt><tt>import Control.Monad.IO.Class (MonadIO)</tt><tt><br>
</tt><tt>import Control.Monad.Trans.Except (ExceptT, runExceptT)</tt><tt><br>
</tt><tt>import Control.Monad.Trans.Reader (Reader, runReader)</tt><tt><br>
</tt><tt>import Control.Monad.Trans.State (StateT, runStateT)</tt><tt><br>
</tt><tt><br>
</tt><tt>type MS c s = ExceptT String (StateT s (Reader c))</tt><tt><br>
</tt><tt><br>
</tt><tt>runMS :: c -> s -> MS c s a -> (Either String
a, s)</tt><tt><br>
</tt><tt>runMS c s f = runReader (runStateT (runExceptT f) s) c</tt><tt><br>
</tt><tt><br>
</tt><tt>f1 :: (MonadIO m) => c -> m ()</tt><tt><br>
</tt><tt>f1 c = do</tt><tt><br>
</tt><tt> let _x1 = run f2</tt><tt><br>
</tt><tt> let _x2 = run f3</tt><tt><br>
</tt><tt> return ()</tt><tt><br>
</tt><tt> where</tt><tt><br>
</tt><tt> run :: MS </tt></font><font color="#ff0000"><tt><b>_c</b></tt></font><font
size="-1"><tt> Int a -> (Either String a, Int) --- failure
or success, 'c' or '_</tt><tt>'<br>
</tt><tt> run = runMS c 0</tt><tt><br>
</tt><tt> f2 :: MS c s Bool</tt><tt><br>
</tt><tt> f2 = pure False</tt><tt><br>
</tt><tt> f3 :: MS c s [Int]</tt><tt><br>
</tt><tt> f3 = pure []</tt><tt><br>
</tt></font><br>
<br>
<br>
</p>
</body>
</html>