[Haskell-cafe] Re: Flipping *->*->* kinds, or monadic finally-tagless madness

[Ahn, Ki Yung]

Kim-Ee Yeoh wrote:
>
> The add function illustrates the kind of do-sugaring we know and love
> that I want to use for Symantics.
> 
>>    lam f   = unZ $ do
>>       show_c0 <- get
>>       let
>>          vname = "v" ++ show_c0
>>          c0 = read show_c0 :: VarCount
>>          c1 = succ c0
>>          fz :: Z a String -> Z b String
>>          fz = Z . f . unZ
>>       put (show c1)
>>       s <- (fz . return) vname
>>       return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
> 
> Now with lam, I get this cryptic error message (under 6.8.2):
> 
>     Occurs check: cannot construct the infinite type: b = a -> b
>     When trying to generalise the type inferred for `lam'
>       Signature type:     forall a1 b1.
>                           (Y String a1 -> Y String b1) -> Y String (a1 ->
> b1)
>       Type to generalise: forall a1 b1.
>                           (Y String a1 -> Y String b1) -> Y String (a1 ->
> b1)
>     In the instance declaration for `Symantics (Y String)'
> 
> Both the two types in the error message are identical, which suggests
> no generalization is needed.  I'm puzzled why ghc sees an infinite type.
> 
> Any ideas on how to proceed?

Not an answer, but just a different error message from GHC 6.10.3 when I 
   tried loading up your code.

kyagrd at kyavaio:~/tmp$ ghci EvalTaglessF.hs
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( EvalTaglessF.hs, interpreted )

EvalTaglessF.hs:264:14:
     Couldn't match expected type `b1' against inferred type `b'
       `b1' is a rigid type variable bound by
            the type signature for `fz' at EvalTaglessF.hs:263:31
       `b' is a rigid type variable bound by
           the type signature for `lam' at EvalTaglessF.hs:248:26
       Expected type: Z b1 String
       Inferred type: Z b String
     In the expression: Z . f . unZ
     In the definition of `fz': fz = Z . f . unZ

EvalTaglessF.hs:264:22:
     Couldn't match expected type `a1' against inferred type `a'
       `a1' is a rigid type variable bound by
            the type signature for `fz' at EvalTaglessF.hs:263:17
       `a' is a rigid type variable bound by
           the type signature for `lam' at EvalTaglessF.hs:248:16
       Expected type: Z a1 String
       Inferred type: Z a String
     In the second argument of `(.)', namely `unZ'
     In the second argument of `(.)', namely `f . unZ'
Failed, modules loaded: none.



I hope this gives you a hint, if any.  I am not exactly sure about how 
to solve this but I might try using scoped type variables extension 
somehow if I were in your shoe.