[Haskell] GHC Error question

[Simon Peyton-Jones]

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