Type families that are not injective give rise to confusing erorrs.

See for an example.

See long error.

```
% ghci-9.2.2 Squeeze.hs
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf
[1 of 1] Compiling Main ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :reload
[1 of 1] Compiling Main ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :type deasilsB . deasilsA
deasilsB . deasilsA
:: (ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
λ deasils = deasilsB . deasilsA

:3:1: error:
• Could not deduce: Dress seed0 peels0 ~ Dress seed peels
from the context: (ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[]))
bound by the inferred type for ‘deasils’:
forall {peels :: [* -> *]} {seed} {value}.
(ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
at :3:1-29
Expected: (Dress seed peels, value) -> Dress (seed, value) peels
Actual: (Dress seed0 peels0, value)
-> Dress (seed0, value) peels0
NB: ‘Dress’ is a non-injective type family
The type variables ‘seed0’, ‘peels0’ are ambiguous
• In the ambiguity check for the inferred type for ‘deasils’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
deasils :: forall {peels :: [* -> *]} {seed} {value}.
(ForAll peels Functor,
Squeezy'
seed
(Dress seed peels)
peels
(Strip seed (Dress seed peels) == '[]),
Squeezy'
(seed, value)
(Dress (seed, value) peels)
peels
(Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
(Dress seed peels, value) -> Dress (seed, value) peels
```

I am not sure how exactly this error message can be improved.

* Maybe the problem is that the error message does not explain where the unsolvable constraint arises from. The process of constraint generation and solving is rather obscure. There is a lot written about type systems, but constraint solving is nowhere mentioned — it is a niche feature that, as far as I can see, was invented specifically for GHC. I am by far not a novice, but nothing in my previous life had prepared me to trace GHC's constraint solver's algorithm with pen and paper. So facing this error was a cognitive dead end.

For example, it would have helped me much if the error message said where precisely the constraint in question arises from. A show of casual inference would be good. In my understanding:

1. An expression _e_ is assigned to the name _n_.
2. The type _t_ of _e_ has type variables _v_.
3. _t_ is constrained by a constraint _c_ that mentions some _v' ⊂ v_.
* Specifically, in this case the constraint _c_ is that _t_ unifies with the type of _n_.
5. In order to solve _c_, GHC has to find what _v'_ are. _(Why?)_
6. _v'_ cannot be inferred from _t_.

I do not think this is the right outline for how this error arises, but it is the best of my understanding after thinking about it for all this time. Maybe we can amend it together and from there see how to improve the error message.

* Maybe the problem is that the error message is actually misleading. Simon thinks that the error message must say something about the unsolvable constraint, but I think it can be explained much simpler:

1. For some type family _F_ mentioned in the type signature of _e_ _(but not in the constraints)_,
2. GHC knows that _F x ~ F x₀_ _(does not matter how)_ and
3. it needs to infer that _x ~ x₀_ _(does not matter why)_, but
4. it cannot do that because
5. it cannot determine that different values of _x_ and _x₀_ cannot ever give rise to the same type _F x = F x₀_.

It is clear from this outline that the source of the problem is the presence of _F_ in the type signature of _e_ _(but not in the constraints)_. It gives a clear direction to the programmer without appealing to the details of the constraint solving algorithm.

It would be ideal if the error message made it clear that this error cannot be solved by any manipulation of contexts. _(It cannot, right?)_ So since the problematic unsolvable constraint mentions unification variables. _(It does, right?)_ Unification variables cannot be named because their names are generated in the constraint solving algorithm. This makes it impossible to add this constraint to the context of _n_. But we should not say _«unification variables»_ because no one knows what that means.

Actually, in the simplest case, the error message should say that a type signature cannot consist entirely of non-injective type families.