[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Simon Peyton-Jones:
> | | However, I think I now understand what you are worried about.   
> It is the
> | | interaction of type families and GHC's generalised type synonyms  
> (i.e.,
> | | type synonyms that may be partially applied).  I agree that it  
> does lead
> | | to an odd interaction, because the outcome may depend on the  
> order in
> | | which the type checker performs various operations.  In  
> particular,
> | | whether it first applies a type instance declaration to reduce a  
> type
> | | family application or whether it first performs decomposition.
> |
> | yes, indeed, thanks! that was the central point of example one.
>
> Aha.
>
> Just to clarify, then, GHC's 'generalised type synonyms' behave like  
> this.
>
> * H98 says that programmer-written types must obey certain  
> constraints:
>        - type synonym applications saturated
>        - arguments of type applications are monotypes (apart from ->)
>
> * GHC says that these constraints must be obeyed only
>        *after* the programmer-written type has been normalised
>        by expanding saturated type synonyms
>
> http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms
>
> I regard this as a kind of pre-pass, before serious type checking  
> takes place, so I don't think it should interact with type checking  
> at all.
>
> I don't think this normalisation should include type families,  
> although H98 type synonyms are a kind of degenerate case of type  
> families.
>
> Would that design resolve this particular issue?

Not quite, but it refines my proposal of requiring that type synonyms  
in the rhs of type instances need to be saturated.  Let me elaborate.

The current implementation is wrong, as it permits

   type S a b = a
   type family F a :: * -> *
   type instance F a = S a

Why do we need to forbid this type instance?  Because it breaks the  
confluence of equality constraint normalisation.  Here are two  
diverging normalisations:

   (1)

     F Int Bool  ~  F Int Char

   ==> DECOMP

     F Int ~ F Int, Bool ~ Char

   ==> FAIL


   (2)

     F Int Bool  ~  F Int Char

   ==> TOP

     S Int Bool  ~  S Int Char

   ==> (expand type synonym)

     Int  ~  Int

   ==> TRIVIAL

However, here is a (somewhat silly) program that does have partially  
applied type synonyms in a type instances' rhs and that is perfectly ok:

   type S a b = a
   type family F (a :: * -> *) b :: * -> *
   type instance F a b = S (S a) b b

This is ok, because we can expand the type synonyms in the rhs of the  
type instance

   S (S a) b b = S a b = a

and get a valid type.

So, the crucial point is that, as you wrote,

> I don't think this normalisation should include type families,  
> although H98 type synonyms are a kind of degenerate case of type  
> families.

The only way to stratify the normalisation of type synonyms and type  
families such that all type synonyms are expanded before any family  
applications are normalised is by requiring that after normalising the  
rhs of a type instance declaration *by itself*, we get a type that  
only contains saturated applications of type synonyms.  (As Claus  
wrote, this is after all what we do for class instance heads.)

Manuel