# Open Type Family Instance Precedence

**URL:** <https://discourse.haskell.org/t/open-type-family-instance-precedence/10194>\
**Category:** Learn\
**Created:** [August 19, 2024, 5:00pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194 "2024-08-19T17:00:21Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![BebeSparkelSparkel](https://avatars.discourse-cdn.com/v4/letter/b/278dde/32.png) [@BebeSparkelSparkel](https://discourse.haskell.org/u/BebeSparkelSparkel)\
**Post date:** [August 19, 2024, 5:00pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/1 "2024-08-19T17:00:22Z")

</div>

Closed type families have precedence and it is very useful for overlapping instances. It would be really useful to have precedence in open type families.

I am sure there is a reason this is not supported, do you know why?

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [August 19, 2024, 5:20pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/2 "2024-08-19T17:20:42Z")

</div>

For one thing, how would you specify the order syntactically, when different instances can be in different compilation units?

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [August 19, 2024, 5:28pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/3 "2024-08-19T17:28:51Z")

</div>

We already have a modular precedence system for infix operators. So we could mirror that: have a fixed number of type family instance precedence levels and specify for each instance which precedence level it has.

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [August 19, 2024, 5:33pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/4 "2024-08-19T17:33:20Z")

</div>

The tricky thing is type soundness, which is imperiled if you allow some type family application `F X` to reduce to `S` in one context and `T` in a different context, because then you can prove `S ~ F X ~ T` and hence write `unsafeCoerce`. Closed type families avoid this by ensuring that a later equation fires only if none of the earlier equations apply (or if they do apply, that the results are consistent).

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [August 19, 2024, 5:36pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/5 "2024-08-19T17:36:50Z")

</div>

> [@adamgundry](#):
>
> because then you can prove `S ~ F X ~ T`

Well, you can prove `S ~ F X` in one context and `F X ~ T` in the other, but I think if you add appropriate checks then I think you can make it so that you can never combine these contexts and get `S ~ T` out of it.

This reminds me of world semantics for type classes (see Section 4.4 of Scott Kilpatrick’s [Non-Reformist Reform for Haskell Modularity](https://people.mpi-sws.org/~skilpat/papers/kilpatrick-thesis-nov-2019-publication.pdf)).

Edit: Actually, @adamgundry can you give an example? I’ve tried this:

```haskell
module A where

type family F a

```

```haskell
module B where

import A

type instance F Bool = Int

```

```haskell
module C where

import A

type instance F Bool = ()

```

And that seems to work properly with a check at import-time:

```haskell
ghci> import B
ghci> import C

<interactive>:1:1: error: [GHC-34447]
    Conflicting family instance declarations:
      A.F GHC.Types.Bool = GHC.Types.Int -- Defined in module B
      A.F GHC.Types.Bool = () -- Defined in module C

```

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [August 19, 2024, 6:30pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/6 "2024-08-19T18:30:52Z")

</div>

> [@jaror](#):
>
> Well, you can prove `S ~ F X` in one context and `F X ~ T` in the other, but I think if you add appropriate checks then I think you can make it so that you can never combine these contexts and get `S ~ T` out of it.

This seems tricky to establish, given that the soundness argument for System FC isn’t aware of such things as module boundaries. Moreover, if a module knows that `S ~ F X`, pretty much any definition it exposes might depend on that fact, and hence be unsafe to compose with definitions from the other module.

> [@jaror](#):
>
> Actually, @adamgundry can you give an example?

My point was that GHC rejects such examples (both on-the-nose conflict as you demonstrate, but also inconsistent overlapping type family instances), because to accept them would be unsound.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [August 20, 2024, 1:11am UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/7 "2024-08-20T01:11:55Z")

</div>

> [@tomjaguarpaw](#):
>
> how would you specify the order syntactically, when different instances can be in different compilation units?

Indeed. What it needs is a way to say: this instance applies except when …; and to express the exception(s) in some sort of a notation that the compiler can examine; so it can check all instances in imports are apart from instances in this module. IOW not merely a precedence system

[Instance Apartness Guards](https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst), which specifically addresses how to handle separate compilation units.

I’ve dummied-up an implementation. It works for me and means instance logic/esp FunDeps is easier to follow IMO

```haskell
class {-# INSTANCEGUARDS #-} Add a b r | a b -> r, r a -> b, r b -> a
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r) | b /~ (Succ r)

```

---

<div class="post-metadata">

**Author:** ![mixphix](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/mixphix/32/5629_2.png) [@mixphix](https://discourse.haskell.org/u/mixphix)\
**Post date:** [August 20, 2024, 2:07pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/8 "2024-08-20T14:07:40Z")

</div>

FWIW the Lean 4 manual has a [section on default instances and instance priorities](https://lean-lang.org/lean4/doc/typeclass.html?highlight=priority#default-instances), so there is certainly prior art. Whether Haskell’s type class system can support this is another story.

---

<div class="post-metadata">

**Author:** ![atravers](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@atravers](https://discourse.haskell.org/u/atravers)\
**Post date:** [August 20, 2024, 9:04pm UTC](https://discourse.haskell.org/t/open-type-family-instance-precedence/10194/9 "2024-08-20T21:04:25Z")

</div>

Prior art for a _strict_ language - it may be easier to reimplement default and prioritised instances in another strict or total language rather than Haskell. `(`Of course, there’s another option: bring laziness to the likes of Lean, Idris, and Agda - any expression not used by dependent types can still be lazy! `:-)`