[Haskell] GHC Error question

[Lennart Augustsson]

And why isn't C a b equivalent to C a b1?
   forall a b . C a b => a -> a
and
   forall a b1 . C a b1 => a -> a
look alpha convertible to me.  Or is the inferred type
   forall a . C a b1 => a -> a

Btw, this reminds me again that I'd like to be able to use _ in type  
signatures.
With the meaning of _ being, "there's a type here, but I can't be  
bothered to write it out in full."

	-- Lennart

On Dec 6, 2006, at 02:46 , Simon Peyton-Jones wrote:

> I agree that this is confusing.  Here is a cut-down example:
>
>         class C a b where
>                 op :: a -> a
>
>         -- f :: C a b => a -> a
>         f x = op x
>
> It doesn't get much simpler than that!  With the type sig, GHC  
> can't see that the (C a b) provided can satisfy the (C a b1) which  
> arises from the call to op.   However, without the constraint, GHC  
> simply abstracts over the constrains arising in the RHS, namely (C  
> a b1), and hence infers the type
>         f :: C a b1 => a -> a
>
> It is extremely undesirable that the inferred type does not work as  
> a type signature, but I don't see how to fix it
>
> Simon
>
> | -----Original Message-----
> | From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow- 
> haskell-users-
> | bounces at haskell.org] On Behalf Of Norman Ramsey
> | Sent: 06 December 2006 01:41
> | To: Simon Peyton-Jones
> | Cc: GHC users
> | Subject: Re: [Haskell] GHC Error question
> |
> |  > [redirecting to ghc users]
> |  >
> |  > It looks like a splendid error to me.
> |
> | I'm not sure if you meant the error or the message was splendid :-)
> | I yelled for help because my usual strategy failed.  That  
> strategy is
> |
> |   1. Remove the type annotation.
> |   2. Get ghci to tell me what the 'right type' is.
> |   3. Put the 'right type' in the type annotation.
> |
> | I find it a bit depressing that the most general type inferred by  
> ghci
> | does not work as a type signature.
> |
> |  > I can't say more without seeing the code.  can you give a  
> small repo case?
> |
> | Yes, here's a case that fits in one screen of emacs :-)
> |
> |
> | {-# OPTIONS -fglasgow-exts #-}
> | module Ccomp where
> |
> | type Name = String
> |
> | data Inface  = N | W
> | data Outface = S | E
> |
> | data Sink   box = Boxin  Inface  box | Result
> | data Source box = Boxout Outface box | Arg Inface
> |
> | data Command = Send0
> |
> | class (Monad b) => Builder b box where
> |   box  :: Command -> b box
> |   wire :: Source box -> Sink box -> b ()
> |
> | type Env box = Name -> Sink box
> |
> | empty = \x -> error (x ++ " not connected or multiply connected  
> in circuit")
> |
> | -- either of these explicit signatures causes the compiler to fail
> | -- although the inferred signature is the second.
> | --compile1 :: (Builder b box) => Name -> Name -> ANF -> b Name
> | compile1 :: (Builder t box) => t1 -> Name -> ANF -> t t1 --  
> generated by ghci
> | compile1 f x body = do env <- compile body empty
> |                        wire (Arg W) (env x)
> |                        return f
> |
> | data ANF = ANF ()
> |
> | compile :: (Builder b box) => ANF -> Env box -> b (Env box)
> | compile (ANF m) out = undefined
> |
> |  > | This program is rejected by GHC with the following message:
> |  > |
> |  > | Ccomp.hs:54:23:
> |  > |     Could not deduce (Builder b box1) from the context  
> (Builder b box)
> |  > |       arising from use of `wire' at Ccomp.hs:54:23-42
> |  > |     Possible fix:
> |  > |       add (Builder b box1) to the type signature(s) for  
> `compile1'
> |  > |     In the expression: wire (Arg W) (env x)
> |  > |     In a 'do' expression: wire (Arg W) (env x)
> |  > |     In the expression:
> |  > |         do env <- compile body empty
> |  > |            wire (Arg W) (env x)
> |  > |            return f
> |  > |
> |  > | Note that compile1 has an explicit type signature much along  
> the lines
> |  > | suggested by GHC.  If I *remove* this type signature, the  
> function
> |  > | compiles successfully, and ghci reporets this type for  
> compile1:
> |  > |
> |  > |   compile1 :: (Builder t box) => t1 -> Name -> Ir.ANF -> t t1
> |  > |
> |  > | I believe this signature is isomorphic to the explicit  
> signature I had
> |  > | attempted to use.
> | _______________________________________________
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users at haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users