[GHC] #12119: Can't create injective type family equation with TypeError as the RHS

25 May 2016

      #12119: Can't create injective type family equation with TypeError as the RHS
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  CustomTypeErrors, TypeFamilies,    |
  Injective                          |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 For the longest time, I've wanted to make a type family like this
 injective:

 {{{#!hs
 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
 `TypeError`s, however, I thought I could rule out all other cases:

 {{{#!hs
 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?

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12119
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler