Applying typed hole proposal leads to compilation failure
Hello Cafe, 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'. Why does GHC think those two are different and how to tell to GHC they are the same? Best regards, vlatko *Typed hole proposal:* • 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 • In the type signature: run :: MS _c Int a -> (Either String a, Int) *Error when typed hole used:* • 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) at Test.hs:21:5-47 ‘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 Expected type: MS c1 Int a -> (Either String a, Int) Actual type: MS c Int a -> (Either String a, Int) * * *Minimal runnable example:* {-# LANGUAGE ScopedTypeVariables, PartialTypeSignatures #-} module Test where import Prelude import Control.Monad.IO.Class (MonadIO) import Control.Monad.Trans.Except (ExceptT, runExceptT) import Control.Monad.Trans.Reader (Reader, runReader) import Control.Monad.Trans.State (StateT, runStateT) type MS c s = ExceptT String (StateT s (Reader c)) runMS :: c -> s -> MS c s a -> (Either String a, s) runMS c s f = runReader (runStateT (runExceptT f) s) c f1 :: (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) --- failure or success, 'c' or '_' run = runMS c 0 f2 :: MS c s Bool f2 = pure False f3 :: MS c s [Int] f3 = pure []
• 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 []
Note that this also requires ScopedTypeVariables; the Haskell standard specifies that type variables are only in scope within the type signature, not the accompanying binding. Which is also why the explicit "forall" is required, to tell it to use the modified rules here, which otherwise could cause other code that expects standard Haskell behavior to fail to compile if it happens to reuse type variables from the signature. On Fri, Aug 24, 2018 at 5:37 PM mniip <14@mniip.com> wrote:
• 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 [] _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- brandon s allbery kf8nh allbery.b@gmail.com
On Fri, Aug 24, 2018 at 06:25:34PM -0400, Brandon Allbery wrote:
Note that this also requires ScopedTypeVariables; the Haskell standard specifies that type variables are only in scope within the type signature, not the accompanying binding. Which is also why the explicit "forall" is required, to tell it to use the modified rules here, which otherwise could cause other code that expects standard Haskell behavior to fail to compile if it happens to reuse type variables from the signature.
I had thought of mentioning this but their original snippet included the extension so I thought they already knew.
Hi mniip, Let me first apologise for my very late response. I went for a visit to the analog world, and stayed much longer than planned. :-) I have ScopedTypeVariables enabled as a default extension in .cabal file, but have never encountered such an error, to have to manually specify forall just for making scoped types to work. I'm using local signatures quite often, but still not quite clear as to how/where the original code differs, for example, from this one (which compiles fine): mkTransUnitValTag :: (HasGlobals s) => InNode -> MS c s TransUnitValT mkTransUnitValTag e@(Element "tuv" as (cleanBlank -> cs) _) = do TransUnitValT <$> attrGlobDef e glbDataType "datatype" as -- tuvDataType ... <*> parseTag e "seg" mkSegTag cs -- tuvSeg where mkSegTag :: InNode -> MS c s Content mkSegTag (Element "seg" _as ss _) = checkContent =<< mapM mkContentTag ss Is the main diff that 'run' is having monad stack as input and is running it, while 'mkSegTag' is run in it (so forall does not have to be specified manually)? mkSegTag :: InNode -> MS c s Content f1 :: forall m c. (MonadIO m) => c -> m () -- original code where run :: MS c Int a -> (Either String a, Int) Thanks for pointing me to read the whole error/warning. Everything is actually written there, but seems I have developed some kind of forall blindness. :-( On 24/08/2018 23:36, mniip wrote:
• 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 [] _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
Brandon Allbery -
mniip -
Vlatko Basic