[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families

[Anthony Clayden]

> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote:

> 
> ... [in] closed type families. (We
> would also have to eliminate non-linear patterns,
> replacing them with some other first-class test for
> equality.

> AntC's proposed disequality constraints then become
> straightforward pattern guards.

Guards don't have to be just disequalities.

If you want to eliminate non-linear patterns,
use _equality_ guards. Full example:

> type family F a b where
>   F a   a    = a
>   F Int b    = b
>   F a   Bool = a
> 

Translates to:

> type instance F a b | a ~ b = a
> type instance F a b | a ~ Int, a /~ b = b
> type instance F a b | b ~ Bool, a /~ Int, a /~ b = a

(Each instance after the first
 has disequality guards to negate the earlier instances'
equalities., i.e. the earlier instances 'shadow' the
overlap.)

> It's currently unclear to me how to do this
> right. ... 
> 

Assuming we have a primitive type-level
equality test (?~), returning type-level Bool;
we can use helper functions.
The first instance desugars to a call

> ... = F_a_b_Eq (a ?~ b) a b

> type instance F_a_b_Eq True a b = a

(Needs UndecidableInstances.)

> Section 5.13.2 of my thesis dwells on this, without
> much in the way of a concrete way forward.)

We use type equality testing all the time.
In fact instance selection relies on it.

5.13.2 says: "they [equality testing rules] cannot handle
 the case where Equals a a reduces to True,
 where a is locally bound type variable."

?? I thought GHC's equality test
requires types to be grounded,
i.e. not merely type vars,
in order to be judged equal.
Or did that change recently?

Isn't that to do with impredicativity
and the dreaded monomorphism:
the same typevar might get a different
forall-qualified type in different use sites.

Contrast types can be judged dis-equal
without necessarily being grounded.
[HList paper section 9 refers.]


AntC