...

On Sun Jun 4 13:11:47 UTC 2017, J. Garrett Morris wrote: ... You keep talking about guarding instances or equations. Guards are equivalent to closed type families,

I think not. They're somewhere between CTFs and Instance Chains. In that guarded instances are not closed. Which also appears to be your claim wrt Instance Chains.

A further difference is wrt class instances and FunDeps. AFAICT, the closed class instances/Partiality paper is expecting no FunDeps, but using Assoc types within the class to achieve the same effect. I agree with that long-term aim, so the following applies to both guarded class instances and guarded type instances. The dreaded "Instances inconsistent with FunDeps" error can be boiled down to:

class TypeEq a b p | a b -> p instance TypeEq a a HTrue instance TypeEq a b HFalse

The check for FunDep consistency unifies the class parameters on LHS of FunDep, yielding subsititution { a ~ b }. Then applies that substitution to rhs. yielding { HTrue ~ HFalse } doesn't hold, so inconsistency. GHC allows you to put this instead:

instance TypeEq a a HTrue -- same instance (p ~ HFalse) => TypeEq a b p

The consistency test compares { p ~ HTrue }, and apparently sees those as unifiable, despite the (~ HFalse) constraint. There are those [for example, Iavor], who think this should still count as inconsistent. So it works (and has consistently since 2004), but seems iffy. Furthermore the bare typevar `p` breaks the Coverage Conditions, (again despite the (~ HFalse) constraint grr! So you need UndecidableInstances, which apparently is not as benign as heretofore thought. With InstanceGuards it goes like this: class {-# INSTANCEGUARDS #-} TypeEq a b p | a b -> p instance TypeEq a a HTrue -- same instance TypeEq a b HFalse | a /~ b Now the consistency check: unifies the class parameters on lhs of FunDep, yielding { a ~ b } as before; then substitutes into the guard, yielding { a /~ a } -- a contradiction. So it doesn't need to check the consistency of the result. Because the 'arguments' to the FunDep are apart. Notice the side-benefit: by putting explicit HFalse, we haven't broken the Coverage Conditions, so don't need UndecidableInstances. The guarded type family goes likewise:

type family {-# INSTANCEGUARDS #-} Equals a b :: Bool type instance Equals a a = True type instance Equals a b | a /~ b = False

AntC