[ ghc-Bugs-1180651 ] Strange GADT behaviour

Bugs item #1180651, was opened at 2005-04-11 11:39
Message generated for change (Comment added) made by simonpj
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1180651&group_id=8032

Category: Compiler (Type checker)
Group: 6.4
Status: Open
Resolution: None
Priority: 5
Submitted By: Josef Svenningsson (josefs)
Assigned to: Nobody/Anonymous (nobody)
Summary: Strange GADT behaviour

Initial Comment:
When I try to get the file Bug.hs to type check I get
the strangest error messages from the type checker.
Just a short explanation of the program. It contains
some class declarations capturing some definitions from
category
theory. Further down he have a data type for well typed
lambda expressions using GADTs. Finally we have a
function defining the semantics for lambda terms called
'interp'.

First of all the file doesn't compile as it stands,
giving me the following error:
<error>
Bug.hs:54:0:
    Quantified type variable `t' is unified with
another quantified type variable terminal
    When trying to generalise the type inferred for
`interp'
      Signature type:     forall terminal
                                 (exp :: * -> * -> *)
                                 (prod :: * -> * -> *)
                                 (arr :: * -> * -> *)
                                 s
                                 t.
                          (CartesianClosed terminal exp
prod arr) =>
                          Lambda terminal exp prod s t
-> arr s t
      Type to generalise: Lambda t exp prod s t -> arr s t
    In the type signature for `interp'
    When generalising the type(s) for `interp'
</error>
I don't understand why this is happening.

If I comment out the first line in the interpreter the
module typechecks. But I *want* that first line.

When I wanted to distill the example other funny things
started to happen. When I comment out the cases for Lam
and App in both the data type and the interpreter I get
the following two errors:
<error>
Bug.hs:53:26:
    Kind error: `exp' is not applied to enough type
arguments
    In the type signature:
      interp :: (CartesianClosed terminal exp prod arr) =>
                Lambda terminal exp prod s t -> arr s t

Bug.hs:56:22:
    Occurs check: cannot construct the infinite type: a
= prod a b
      Expected type: arr (prod a b) b
      Inferred type: arr (prod (prod a b) b1) b
    In the expression: first `comp` (interp (Var v))
    In the definition of `interp':
        interp (Var (S v)) = first `comp` (interp (Var v))
</error>

----------------------------------------------------------------------

>Comment By: Simon Peyton Jones (simonpj)
Date: 2005-04-15 15:52

Message:
Logged In: YES 
user_id=50165

I've had a look.  There are several going on here.

Your original problem is the same as others have 
encountered; GHC isn't solving class constraints early 
enough, and isn't applying functional dependencies locally 
enough.  In this particular case, in the Unit branch, we have 
terminal=t, and GHC ends up with a Terminal t arr constraint.  
Then, at the outer level we have (Terminal t arr) from the Unit 
branch, and (Terminal terminal arr) from the signature 
(superclass of CartesianClosed), so t gets unified with arr.  
It's a bug.

The kind problem is correct, but a bad error message.  WHen 
you comment out the constructors, GHC infers a kind of * for 
the exp argument of Lambda, and that doesn't fit with its use 
in the type siguature.  But the error message is bad.

I have no clue what is going on with the second error 
message; I think it is caused by the fact that the compiler 
should bale out when it finds the kind error. If it carries on, all 
manner of strange things might happen, and clearly do.  So 
that's another bug really.  

Three bugs in one.  Well done!  

Combining GADTs with classes and fundeps is obviously 
going to be important, so I should up the priority on it!

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1180651&group_id=8032