[Haskell-cafe] Equality constraints in type families

[Claus Reinke]

>> type family F a :: * -> *
..
> 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

i'm still trying to understand this remark:

- if we are talking about "type functions", i should be allowed
    to replace a function application with its result, and if that
    result doesn't mention some parameters, they shouldn't
    play a role at any stage, right?

- if anything other than the function result matters, isn't it
    somewhat misleading to speak of "type functions"?

- if the parameters have to match irrespective of whether
    they appear in the result, that sounds like phantom types.

    ok, but we're talking about a system that mixes unification
    with rewriting, so shouldn't the phantom parameters be
    represented in all rewrite results, just to make sure they
    cannot be ignored in any contexts?

    ie, with

    type instance F a = <rhs>

    F a x should rewrite not to <rhs>, but to <rhs>_x,
    which would take care of the injectivity you want in the
    ~-case, but would also preserve the distinction if 
    rewriting should come before ~, even if <rhs> managed
    to consume x, by being a constant function on types. 

- things seem to be going wrong in the current implementation.
    consider this code, accepted by GHCi, version 6.9.20080317:
------------------------------------------
{-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> *
type instance Const a = C a
type C a t = a

f :: Const Bool Int -> Const Bool Char -> Const Bool Bool
f i c = False
-- f i c = i
f i c = i && True
f i c = (i || c) 
------------------------------------------

    (note the partially applied type synonym in the type instance,
    which is a constant function on types). it looks as if:

    - False::Bool is accepted as Const Bool Bool
    - i::Const Bool Int is accepted as Bool
    - c::Const Bool Char is accepted as Bool
    - both i and c are accepted as Bool, so seem to be of
        an equivalent type, but aren't really..
    - i::Const Bool Int is not accepted as Const Bool Char
        directly, but is accepted via one of the "eta expansions" 
        for Bool, namely (&&True)

my current guess is that the implementation is incomplete,
but that the idea of "type functions" also needs to be adjusted
to take your design decision into account, with "phantom types"
and type parameter annotations for type function results 
suggesting themselves as potentially helpful concepts?

or, perhaps, the implication isn't quite correct, and 
type parameters shouldn't be unified unless they appear
in the result of applying the type function? the implementation
would still be incomplete, but instead of rejecting more of the
code, it should allow the commented-out case as well?

could you please help me to clear up this confusion?-)

thanks,
claus