[Haskell-cafe] Type Instance Partiality [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

> 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