Dan Doel:
On Tuesday 11 March 2008, Tom Schrijvers wrote:
I think you've uncovered a bug in the type checker. We made the
design
choice that type functions with a higher-kinded result type must be
injective with respect to the additional paramters. I.e. in your
case:
F x y ~ F u v <=> F x ~ F u /\ y ~ v
So if we apply that to F d c ~ F a (c,a) we get:
F d ~ F a /\ c ~ (c,a)
where the latter clearly is an occurs-check error, i.e. there's no
finite
type c such that c = (c,a). So the error in the second version is
justified. There should have been one in the latter, but the type
checker
failed to do the decomposition: a bug.
While I think I understand why this is (due to the difference
between index
and non-index types), does this mean the following won't type check
(it does
in 6.8, but I gather its type family implementation wasn't exactly
complete)?
type family D a :: *
type family E a :: *
type instance D Int = Char
type instance D Char = Int
type instance E Char = Char
type instance E Int = Int
type family F a :: * -> *
type instance F Int = D
type instance F Char = E
foo :: F Int Int ~ F Char Char => a
foo = undefined
Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither
Int ~ Char
nor F Int ~ F Char.
Then again, looking at that code, I guess it's an error to have D
and E
partially applied like that?
Exactly.
And one can't write, say:
type instance F Int a = D a
correct? I suppose that clears up situations where one might be able
to
construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at
least, I
can't thing of any others off the top of my head).
Yes, this type instance is invalid. However, early version of the
type family implementation erroneously accepted such instances.
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
