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

21 Jun 2017

      #12119: Can't create injective type family equation with TypeError as the RHS
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:
      Resolution:                    |  CustomTypeErrors, TypeFamilies,
                                     |  InjectiveFamilies
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 RyanGlScott):

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

 {{{#!diff
 diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
 index cabfb33..b56b68e 100644
 --- a/compiler/typecheck/FamInst.hs
 +++ b/compiler/typecheck/FamInst.hs
 @@ -42,6 +42,7 @@ import VarSet
  import Bag( Bag, unionBags, unitBag )
  import Control.Monad
  import NameEnv
 +import PrelNames
  import Data.List

  #include "HsVersions.h"
 @@ -712,10 +713,13 @@ makeInjectivityErrors fi_ax axiom inj conflicts
                                 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.

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