[ ghc-Bugs-1180651 ] Strange GADT behaviour

[SourceForge.net]

Bugs item #1180651, was opened at 2005-04-11 13:39
Message generated for change (Tracker Item Submitted) made by Item Submitter
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>

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

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