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
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
