[Haskell-cafe] Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

> > 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