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>
