In GHC ticket #5590, I proposed some new syntactic sugar with an elaborative semantics. The objective is to make it easier to use type families for instance selection.

SPJ commented:

I’m afraid I do not understand the proposal in this ticket, yet anyway; an example or two doesn’t tell me its syntax, static semantics, internal language, or dynamic semantics.

I’m writing this post to emphasize that my proposal is technically just a new syntax with an elaboration semantics. I’ll still start with another example, but it’s a better one than I used in the ticket description. I’ll close with a more formal take on the proposed syntax and its elaboration semantics.

There are plenty of simpler examples of this technique, but I’m sharing an example here that

- uses rather familiar notions,
- I find compelling, and
- demonstrates the idea both for a class and for a type family.

In combination with total type families (possibly implemented via NewAxioms), this sugar could succinctly supplant much of the functionality of `OverlappingInstances`

— stare deep into the Oleg.

## Motivating Example

(Full code on hpaste.)

Consider writing a `Functor`

instance for the `* -> *`

composition type, `:.:`

.

newtype (:.:) (f :: * -> *) (g :: * -> *) = Comp {unComp :: f (g a)}

The wrinkle with writing a `Functor`

instance for `:.:`

is that there are two equally valid implementations, but they are syntactically ambiguous. Because they have identical instance *heads*, GHC won’t allow both of them. Conal Elliott laments this problem in the `type-compose`

package.

class Contra f where contramap :: (a -> b) -> f b -> f a

```
```instance (Functor f, Functor g) => Functor (f :.: g) where

fmap f = Comp . fmap (fmap f) . unComp

`instance (Contra f, Contra g) => Functor (f :.: g) where`

fmap f = Comp . contramap (contramap f) . unComp

### Solution with current GHC syntax

Here’s a solution to this wrinkle that I consider to be the most direct. My basic proposal in #5590 merely eliminates the syntactic overhead of this workaround — it involves no new semantics or expressivity.

The two `Functor`

instances are distinguished semantically based on the variance of `f`

(or of `g`

— it seems to be a stylistic choice). This semantic information is not present in the instance head, so GHC cannot distinguish the instances. The distinction *is present* in the constraints, but GHC ignores those during instance selection.

The idea of using the instance contexts to differentiate instances raises even more issues, because of the various extensions to instances like `Overlapping`

or `Incoherent`

. Type families, on the other hand, do not raise such issues because their instances are more restricted than are class instances. So we turn to type families.

We encode variance, the property we wish to use to distinguish our two `Functor`

instances, as a type family. We’ll keep it simple for now and consider only co- and contra-variant parametric data types.

{-# LANGUAGE DataKinds, PolyKinds #-} -- etc.

```
```data V = CoV | ContraV -- datakind for variance; see footnote [1]

data PROXY a = PROXY -- polykinded proxy, for passing types explicitly

-- polykinded variance w.r.t. the next argument of t

type family Variance (t :: kD -> kR) :: V

`type instance Variance [] = CoV`

type instance Variance Maybe = CoV

type instance Variance (->) = ContraV

type instance Variance ((->) a) = CoV -- etc.

We’ll need an example contravariant type of kind `* -> *`

.

newtype IntSink a = IntSink (a -> Int)

```
```

`type instance Variance IntSink = ContraV`

instance Contra IntSink where

contramap f (IntSink x) = IntSink (x . f)

This is the type for which we need that second `Functor`

instance, the one that uses `Contra`

. For example, our goal is to make the `test`

function below well-typed.

ex :: (IntSink :.: IntSink) String

ex = Comp $ IntSink $ \(IntSink sink) -> sink "payload"

```
```

`test :: (IntSink :.: IntSink) Int`

test = fmap length ex

The well-typedness of `test`

requires the instance `Functor (IntSink :.: IntSink)`

.

All of the code up to this point is motivation for the example; we’re just now getting into the bits relevant to #5590.

Using the `Variance`

type family, we declare an auxiliary class that accommodates our two instances with distinct instance heads.

class Functor_V f (v :: V) where

fmap_V :: PROXY v -> (a -> b) -> f a -> f b

```
```instance (Functor f, Functor g) => Functor_V (f :.: g) CoV where

fmap_V _ f = Comp . fmap (fmap f) . unComp

`instance (Contra f, Contra g) => Functor_V (f :.: g) ContraV where`

fmap_V _ f = Comp . contramap (contramap f) . unComp

Note that `Functor_V`

is totally determined by `Functor`

and our choice to branch based on `Variance`

. The method bodies are thus just transliterations of our intended `Functor`

instances. We include the additional `PROXY`

argument so that the method’s type determines all of the class parameters.

Finally, we declare the instance of `Functor`

for `:.:`

by delegating to the auxiliary class `Functor_V`

.

{-# LANGUAGE ScopedTypeVariables #-}

```
```

`instance (fvar ~ Variance f, Functor_V f g fvar) =>`

Functor (f :.: g) where

fmap = fmap_V (PROXY :: PROXY fvar)

Problem solved; our objective function `test`

now type-checks as-is.

### Not just for classes

Left-nestings of `:.:`

will require an instance of `Variance`

for `:.:`

. We can use the same approach for the instance of `Variance`

for `:.:`

that we used for its `Functor`

instance: use an auxiliary family indexed by `V`

.

type instance Variance (f :.: g) = Variance_V (f :.: g) (Variance f)

```
```type family Variance_V (a :: kD -> kR) (v :: V) :: V

type instance Variance_V (f :.: g) CoV = Variance g

type instance Variance_V (f :.: g) ContraV = NegateV (Variance g)

`type family NegateV (v :: V) :: V`

type instance NegateV CoV = ContraV

type instance NegateV ContraV = CoV

Both `Variance_V`

and `Functor_V`

just get an additional parameter. And both `Variance (f :.: g)`

and `Functor (f :.: g)`

instances just delegate to the `*_V`

counterpart by passing in the appropriate `V`

argument. These are two instantiations of the general technique:

Delegate to an auxiliary class/family that dispatches based on the result of a relevant type family.

My proposal in #5590 is syntactic sugar for that technique.

### Solution with the proposed syntax

In the new syntax, we would write the following instead of the `Functor_V`

class, its instances, and the delegating `Functor`

instance for `:.:`

.

guarded instance Functor (f :.: g) with (Variance f)

```
```instance (Functor f, Functor g) => Functor (f :.: g) with CoV where

fmap f = Comp . fmap (fmap f) . unComp

`instance (Contra f, Contra g) => Functor (f :.: g) with ContraV where`

fmap f = Comp . contramap (contramap f) . unComp

It’s much the same for type instances; the following replaces the `Variance_V`

class and its instances as well as the `Variance`

instance for `:.:`

.

type guarded instance Variance (f :.: g) with (Variance f)

```
```

`type instance Variance (f :.: g) with CoV = Variance g`

type instance Variance (f :.: g) with ContraV = NegateV (Variance g)

There are three major benefits of this syntax.

- The user isn’t required to invent names for the auxiliary class/family and duplicate the methods’ signatures.
- Instance selection is still straight-forward: a
`guarded instance`

just forces a bit of type computation and then proceeds with an extra type parameter. - Everything remains open. In our example, the kind of the
`with`

parameter is closed since it’s a datakind. If it instead involved`*`

, new`with`

-instances could be declared as usual.

## The New Syntax

My proposal enriches the notion of *instance head* (involving the new keyword `with`

) and adds a new declaration form (involving the new keyword `guarded`

).

In this rest of this post, I only discuss guarded instances of classes. Guarded instance of families are always simpler.

The definition of *instance head* is enriched to allow zero or more *with-clauses* on the end. A with-clause is the keyword `with`

follow by one or more type expressions, which are separated syntactically in the same way as the parameters of a multi-parameter type class. These type expressions are called with arguments. Each occurrence of `with`

in an instance head associates to the left; the left argument of a with-clause is called its *source*. For example, `(a, b) with E1 with E2`

is a with-clause `E2`

and its source `(a, b) with E1`

. As a result of enriching instance heads, all instance declarations can now include zero or more with-clauses at the end of their head.

Each guarded instance has the syntactic form

`guarded instance Θ => H with T`

._{0} T_{1} … T_{n}

`n`

must be positive. `Θ`

is an instance context, `H`

is the head of the guarded instance (and possibly includes further with-clauses), and each `T`

is a type expression. All type variables occurring in those _{i}`T`

s must be bound by _{i}`H`

or `Θ`

.

### Well-formedness

Any instance (guarded or vanilla) with a with-clause in its head has a head of the shape `H with Ω`

. For this instance head to be well-formed, there must be a guarded instance in scope of the shape `H`

where _{g} with Ω_{g}`H`

is an instance of `H`

with the substitution σ and _{g}`Ω`

is of the same kind as the application of σ to `Ω`

._{g}

### Elaboration semantics

Every guarded instance `guarded instance Θ => H with Ω`

elaborates to two conventional declarations. Let `C`

be `H`

's class. The first generated declaration is an auxiliary class `C'`

that is a fresh copy of `C`

with a new parameter for each type in Ω (added after the existing parameters) and a new `PROXY`

argument in every method for each new class parameter. The second generated declaration is an instance of `C`

with context `(Θ, H[C'/C] Ω)`

that defines each method by applying the corresponding method of `C'`

to the appropriately typed proxy arguments.

Every instance with a head that includes with-clauses `Θ => H with Ω`

elaborates to a single conventional instance `(Θ, Θ`

, where _{g}') => H[C'/C] Ω`C'`

and `Θ`

are determined by the corresponding guarded instance for _{g}`H`

.

Using polykinds, the elaborator could more efficiently re-use class copies that require the same number of additional parameters.

## Conclusion

I’m confident this discussion is better than my original ticket, but it still seems to make it overly complicated. I’m only proposing a little sugar for the underlying technique that uses type families to encode richer instance selection. On the other hand, that technique isn’t even well-known or particularly simple. What can I say? It has worked pretty well for me, and I’d like to be able to use it with less syntactic overhead. YMMV.

Thanks for reading along! Please let me know what you think.

[1] — While I’ve kept the definition of `V`

minimal for this example, it should in general be at least a complete lattice with four elements, co-, contra-, in-, and non-variance. Invariance is both co- and contra-, like `a -> a`

; non-variance is neither co- nor contra-. NB even this lattice is insufficient for some higher-order data types, like `data X a f = X (f a)`

, where the variance w.r.t. one parameter depends on the variance of a later parameter. I’m not sure how `Variance`

interacts with non-parametric types (= indexed? or >= indexed?).