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