[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Mar 25 22:57:48 EDT 2008
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
More information about the Haskell-Cafe
mailing list