On Wed May 17 11:58:24 UTC 2017, Anthony Clayden wrote:

...

On Mon May 15 16:20:09 UTC 2017, Richard Eisenberg wrote:

...

...

...

See my recent draft paper ...

Yes I can see the sense in grounding type family instances with class instances as Associated Types.

Errk I see a fly in the ointment with these 'closed classes'/associated types. Suppose: A class with two assoc types * One assoc type needs the instances in a specific sequence. * The other assoc type needs the instances in a different sequence. Here's a simple (as in daft!) example:

{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleInstances #-}

class (Flip a ~ b, Flop b ~ a) => FlipMaybe a b where type Flip a type Flop b instance (a' ~ b) => FlipMaybe (Maybe a') b where type Flip (Maybe a') = a' type Flop b = Maybe b instance (a ~ b') => FlipMaybe a (Maybe b') where type Flip a = Maybe a type Flop (Maybe b') = b'

(If we wrote a closed class in that sequence, it would get `Flip` right but `Flop` wrong.) Those instances overlap at `FlipMaybe (Maybe a') (Maybe b')`, but we can't write a coherent instance for that overlap. (Using Instance Chains, we'd want a `Fail`.) This is how the instances would go with guards:

{-# LANGUAGE ..., InstanceGuards #-}

instance (a' ~ b) => FlipMaybe (Maybe a') b | b /~ (Maybe _) where type Flip (Maybe a') = a' type Flop b | b /~ (Maybe _) = Maybe b instance (a ~ b') => FlipMaybe a (Maybe b') | a /~ (Maybe _) where type Flip a | a /~ (Maybe _) = Maybe a type Flop (Maybe b') = b'

Note these don't overlap (taking guards into account). IOW we get no available instance for the overlap above.

...

it's really proposing dropping type families in favor of functional dependencies -- but only for partial type families. ...

BTW, while exploring that daft example, I kinda got it to work by declaring `Flip`, `Flop` as stand-alone closed families. But had trouble with the (~) constraints on the class. I changed them to bidirectional FunDeps | a -> b, b -> a and all worked OK. With superclass `(Flop b ~ a)` ghc 8.0.1 complained Couldn't match type ‘Flop b’ with ‘Maybe b’ arising from the superclasses of an instance declaration • In the instance declaration for ‘FlipMaybe (Maybe a') b’ and contrariwise for `(Flip a ~ b)` This is perhaps similar to trac #9918 that you mention in the partiality paper. AntC