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

[Edward Kmett]

Actually the problem lies in your definition of fz, it has the wrong type to
be used in lam.
The Z you get out of fz as type Z b String, but you need it to have Z (a ->
b) String so that when you strip off the Z you have a Y String (a -> b)
matching the result type of lam.

To get there replace your definition of fz with:

> fz :: Z a String -> Z (a -> b) String
> fz = Z . Y . unY . f . unZ

In 6.10.2 I used {-# LANGUAGE FlexibleInstances, TypeSynonymInstances,
MultiParamTypeClasses, ScopedTypeVariables  #-}

and that compiled just fine.

On Thu, Jul 2, 2009 at 8:02 PM, Ahn, Ki Yung <kyagrd at gmail.com> wrote:

> 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.
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090702/08e1cf0e/attachment.html