#12119 closed feature request (wontfix)
Can't create injective type family equation with TypeError as the RHS
Reported by:  RyanGlScott  Owned by:  

Priority:  normal  Milestone:  
Component:  Compiler (Type checker)  Version:  8.0.1 
Keywords:  CustomTypeErrors, TypeFamilies, InjectiveFamilies  Cc:  jstolarek, goldfire, Iceland_jack, sheaf 
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  None/Unknown  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  
Wiki Page: 
Description
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 noninjective. With the introduction of TypeError
s, 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 righthand 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?
Change History (10)
comment:1 Changed 3 years ago by
comment:2 Changed 2 years ago by
Keywords:  InjectiveFamilies added; Injective removed 

comment:3 Changed 2 years ago by
Note: this can be implemented in a deadsimple way:

compiler/typecheck/FamInst.hs
diff git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index cabfb33..b56b68e 100644
a b import VarSet 42 42 import Bag( Bag, unionBags, unitBag ) 43 43 import Control.Monad 44 44 import NameEnv 45 import PrelNames 45 46 import Data.List 46 47 47 48 #include "HsVersions.h" … … makeInjectivityErrors fi_ax axiom inj conflicts 712 713 2 (vcat (map (pprCoAxBranch fi_ax) eqns)) 713 714 , coAxBranchSpan (head eqns) ) 714 715 errorIf p f = if p then [f err_builder axiom] else [] 715 in errorIf are_conflicts (conflictInjInstErr conflicts ) 716 ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs) 717 ++ errorIf tf_headed tfHeadedErr 718 ++ errorIf wrong_bare_rhs (bareVariableInRHSErr bare_variables) 716 in case rhs of 717 TyConApp tc _ 718  tyConName tc == errorMessageTypeErrorFamName > [] 719 _ > errorIf are_conflicts (conflictInjInstErr conflicts ) 720 ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs) 721 ++ errorIf tf_headed tfHeadedErr 722 ++ 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.
comment:4 Changed 2 years ago by
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 userfacing change.
comment:5 Changed 23 months ago by
Resolution:  → wontfix 

Status:  new → closed 
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 = CharBut the problem is that
Foo
is defined on all types of kind*
, so the above definition is inherently noninjective.
But the "inherently noninjective" 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.
comment:6 followup: 8 Changed 11 months ago by
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).
comment:7 Changed 11 months ago by
Cc:  Iceland_jack added 

comment:8 Changed 11 months ago by
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
catchall 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.
comment:9 Changed 11 months ago by
Cc:  sheaf added 

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 a stuck type family application. In my opinion, one of the advantages of injectivity annotation is that internal use of the type family doesn't end up leaking into the frontend.
comment:10 Changed 11 months ago by
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 existentiallyquantified 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 errorhandling logic, that preserves plain n
on the rhs, then that would be injective.
That looks plausible to me.
What is the consequences of declaring
Foo
to be injective? Answer, only that if we havewhere
[W]
means "wanted", a constraint we are trying to solve, then we try to proveAssuming we succeed, binding
g2 = <some coercion>
, then we can prove the first constraint by bindingg1 = Foo g2
.If
F
is not injective, this proof strategy is no unsound; but it may be incomplete. Perhaps there are unequal typest1
andt2
for whichFoo 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 constraintFoo t1 ~ Foo t2
that does not requiret1 ~ t2
. But if the proof goes viaTypeError
, 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.