[Haskell-cafe] Applying typed hole proposal leads to compilation failure

[Vlatko Basic]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180903/cfd4e67f/attachment.html>