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

[kindaro]

See https://gitlab.haskell.org/ghc/ghc/-/issues/21691 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

<interactive>: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 <interactive>: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.
  4. In order to solve c, GHC has to find what v' are. (Why?)
  5. 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.