#12119: Can't create injective type family equation with TypeError as the RHS -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | CustomTypeErrors, TypeFamilies, | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12119#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler