Re: [GHC] #349: Strange GADT behaviour

[GHC]

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

  * resolution:  None => fixed
  * status:  assigned => closed

Comment:

 This bug is fixed, now that I have added implication constraints to GHC.
 At least, the test program works fine in the HEAD.

 Simon

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [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:   | Difficulty:  Unknown 
 Testcase:  gadt/josef   |   Architecture:  Unknown 
   Os:  Unknown  |  
-+--
Changes (by simonpj):

  * testcase:  => gadt/josef

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [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:
> 
> 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'
> 
> 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:
> 
> 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))
> 
> }}}

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:
 
 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'
 
 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:
 
 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