[GHC] #349: Strange GADT behaviour

[GHC]

#349: Strange GADT behaviour
--------------------------------------+-------------------------------------
  Reporter:  josefs                   |          Owner:  simonpj 
      Type:  bug                      |         Status:  assigned
  Priority:  normal                   |      Milestone:  6.8     
 Component:  Compiler (Type checker)  |        Version:  6.4     
  Severity:  normal                   |     Resolution:  None    
  Keywords:                           |             Os:  Unknown 
Difficulty:  Unknown                  |   Architecture:  Unknown 
--------------------------------------+-------------------------------------
Changes (by simonpj):

  * architecture:  => Unknown
  * difficulty:  => Unknown
  * milestone:  => 6.8
  * os:  => Unknown

Old description:

> {{{
> 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>
> }}}

New description:

 {{{
 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>
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/349>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler