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