[GHC] #15549: Core Lint error with EmptyCase

[GHC]

#15549: Core Lint error with EmptyCase
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: goldfire (added)


Comment:

 The culprit here appears to be
 [http://git.haskell.org/ghc.git/blob/21f0f56164f50844c2150c62f950983b2376f8b6:/compiler/simplCore/Simplify.hs#l2566
 improveSeq]. In particular, in its use of `topNormaliseType_maybe`:

 {{{
 improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
            -> OutExpr -> InId -> OutId -> [InAlt]
            -> SimplM (SimplEnv, OutExpr, OutId)
 -- Note [Improving seq]
 improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
   | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
   = do { case_bndr2 <- newId (fsLit "nt") ty2
         ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing
               env2 = extendIdSubst env case_bndr rhs
         ; return (env2, scrut `Cast` co, case_bndr2) }
 }}}

 In the program in comment:1, `scrut` is `x` (from `sTo`), and `idType
 case_bndr1` is `Sing (Rep Void) r` (where `(r :: Rep Void)`). It's
 `topNormaliseType_maybe`'s job to reduce the two type families in `Sing
 (Rep Void) r` (in particular, `Rep Void ~# Void` and then `Sing Void ~#
 R:SingVoidz`) and return the coercion that witnesses this reduction.
 However, it appears to produce an entirely bogus coercion:

 {{{
 Sing (D:R:RepVoid[0]) <r>_N)_R ; D:R:SingVoidz0[0] <r>_N
   :: (Sing (Rep Void) r) ~R# (R:SingVoidz r)
 }}}

 Why is this bogus? Because in the axiom `D:R:SingVoidz0[0]`, we have:

 {{{
 COERCION AXIOMS
   axiom Bug.D:R:SingVoidz0 ::
     forall {z :: Void}.
       Sing Void z = Bug.R:SingVoidz -- Defined at ../Bug.hs:11:15
 }}}

 Notice that the argument to `D:R:SingVoidz0[0]` is of type `Void`, but in
 the coercion above, we're giving it `r` as an argument, which is of type
 `Rep Void`, not `Void`! Unsurprisingly, utter pandemonium ensues when Core
 Lint inspects this garbage.

 The proper coercion would be something like what the second program in
 comment:1 produces:

 {{{
 (Sing (D:R:RepVoid[0]) (GRefl nominal r (D:R:RepVoid[0])))_R ;
 D:R:SingVoidz0[0] <(r |> D:R:RepVoid[0])>_N
   :: (Sing (Rep Void) r :: *) ~R# (R:SingVoidz (r |> D:R:RepVoid[0]) :: *)
 }}}

 Alas, `topNormaliseType_maybe` doesn't produce this. goldfire, do you
 think the reason that this doesn't happen is due to the same underlying
 reasons as in #14729? I strongly suspect that this is the case, since I
 tried calling `normaliseType` on `Sing (Rep Void) r`, and it produces the
 same bogus coercion that `topNormaliseType_maybe` did.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15549#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler