Can't create injective type family equation with TypeError as the RHS

[RyanGlScott]

For the longest time, I've wanted to make a type family like this injective:

type family Foo (a :: *) :: * where
  Foo Bar = Int
  Foo Baz = Char

But the problem is that Foo is defined on all types of kind *, so the above definition is inherently non-injective. With the introduction of TypeErrors, however, I thought I could rule out all other cases:

import GHC.TypeLits

type family Foo (a :: *) = (r :: *) | r -> a where
  Foo Bar = Int
  Foo Baz = Char
  Foo _   = TypeError ('Text "boom")

But this doesn't work, sadly:

Injective.hs:18:3: error:                                                                 
    • Type family equations violate injectivity annotation:                               
        Foo Bar = Int -- Defined at Injective.hs:18:3                                     
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      Type variable ‘_’ cannot be inferred from the right-hand side.
      In the type family equation:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

From GHC's perspective, TypeError is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being TypeError is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that Foo a ~ Foo b (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that a ~ b.

Could this be accomplished by simply adding a special case for TypeError in the injectivity checker?

[simonpj]

That looks plausible to me.

What is the consequences of declaring Foo to be injective? Answer, only that if we have

 [W] g1 : Foo t1 ~ Foo t2

where [W] means "wanted", a constraint we are trying to solve, then we try to prove

 [W] g2: t1 ~ t2

Assuming we succeed, binding g2 = <some coercion>, then we can prove the first constraint by binding g1 = Foo g2.

If F is not injective, this proof strategy is no unsound; but it may be incomplete. Perhaps there are un-equal types t1 and t2 for which Foo t1 ~ Foo t2.

In your example, it's true that Foo Int ~ TypeError "boom" ~ Foo Bool. So indeed there may be a solution to the constraint Foo t1 ~ Foo t2 that does not require t1 ~ t2. But if the proof goes via TypeError, as here, perhaps that particular sort of incompleteness doesn't matter.

So it sounds plausible. I don't really know how to formalise it though.

[RyanGlScott]

Note: this can be implemented in a dead-simple way:

compiler/typecheck/FamInst.hs

@@ -42 +42 @@
 import Bag( Bag, unionBags, unitBag )
 import Control.Monad
 import NameEnv
+import PrelNames
 import Data.List
 
 #include "HsVersions.h"
@@ -712 +713 @@
                                2 (vcat (map (pprCoAxBranch fi_ax) eqns))
                           , coAxBranchSpan (head eqns) )
         errorIf p f     = if p then [f err_builder axiom] else []
-     in    errorIf are_conflicts  (conflictInjInstErr     conflicts     )
-        ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
-        ++ errorIf tf_headed       tfHeadedErr
-        ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)
+     in case rhs of
+          TyConApp tc _
+            | tyConName tc == errorMessageTypeErrorFamName -> []
+          _ ->    errorIf are_conflicts  (conflictInjInstErr     conflicts     )
+               ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
+               ++ errorIf tf_headed       tfHeadedErr
+               ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)

Of course, there's still Simon's point about formalizing this idea, which I have yet to do.

[simonpj]

Of course, there's still Simon's point about formalizing this idea, which I have yet to do.

Yes: formalising it at least into a GHC propoosal would be good: it's a user-facing change.

[RyanGlScott]

It just occurred to me that the entire premise of this ticket is wrong. I claimed:

Replying to RyanGlScott:

For the longest time, I've wanted to make a type family like this injective:

type family Foo (a :: *) :: * where
  Foo Bar = Int
  Foo Baz = Char

But the problem is that Foo is defined on all types of kind *, so the above definition is inherently non-injective.

But the "inherently non-injective" part is totally bogus! In fact, as the code below demonstrates, Foo can be made injective quite easily:

{-# LANGUAGE TypeFamilyDependencies #-}

data Bar
data Baz

type family Foo (a :: *) = (r :: *) | r -> a where
  Foo Bar = Int
  Foo Baz = Char

I don't know why I believed that crazy misconception about injectivity vis-à-vis exhaustivity, but in any case, the entire reason why I was pursuing this feature in the first place has vanished. In light of this, I don't think it's worth adding this much extra complexity to the type family injectivity checker.

[sheaf]

What about the following:

data Dim
  = D2
  | D3
  | D4

type family ToDim (n :: Nat) = d | d -> n where
  ToDim 2 = D2
  ToDim 3 = D3
  ToDim 4 = D4
  ToDim n = TypeError 
    ( Text "Error: dimension must be 2, 3 or 4 (given: "
     :<>: ShowType n :<>: Text ")" )

This seems useful to me, as it allows one to switch easily between two different representations of dimension (which have different uses: with Nats I can do arithmetic, but the explicit enum is more convenient with singletons for instance).

I feel like the injectivity annotation should be allowed in this case (but I am not aware of any of the theory which backs injective type families).

[AntC]

Replying to sheaf:

What about the following: ...

This seems useful to me, ...

Sure, it's the same structure as the O.P.

I feel like the injectivity annotation should be allowed in this case ...

It is. Ryan's comment:5 says what's not allowed is the TypeError catch-all equation -- that is, if you want ToDim to be injective.

So if you call ToDim 5, inference will get stuck, and you'll get an error message somewhere/somehow else.

[sheaf]

I understand that the type family is injective if I remove the type error. However I would prefer a custom error message, as opposed to the user getting some confusing error about stuck type families.

[AntC]

The injectivity annotation is a promise that all your equations are injective.

Then consider the return type of ToDim 5 compared to ToDim 6 (if you put a TypeError equation): they're the same type. Then that equation is not injective.

Specifically, ShowType n is not injective: ​it's an existentially-quantified data constructor, promoted to a datakind.

If you omit the TypeError equation, there's an implicit ToDim n = ToDim n added at the end. That is injective.

Possibly you could put some other error-handling logic, that preserves plain n on the rhs, then that would be injective.