GHC stubbornly produces dead code for empty case with type family

Consider the following instance:

data Void
instance Generic Void where
  type Rep Void = V1
  from x = case x of
  to x = case x of

The pattern checker, when enabled, correctly determines that both from and to cover all cases. Yay! In order to do this, it has to reduce the Rep Void type family application.

The optimizer, on the other hand, does not perform this reduction, presumably because it is not known to terminate. Unfortunate in this case, but fine, I suppose. Here's where it gets really unfortunate. If I write

  to (x :: V1 r) = case x of

then the type checker already has to do the work of unifying Rep Void with V1 r, but the optimizer doesn't take advantage of it! With -O2 -ddump-simpl ..., I get

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl_r2IT :: Addr#
lvl_r2IT = "Phantom.hs:18:20-23|case"#

-- RHS size: {terms: 2, types: 2, coercions: 0, joins: 0/0}
$fGenericVoid1 :: Void
$fGenericVoid1 = patError lvl_r2IT

-- RHS size: {terms: 6, types: 7, coercions: 0, joins: 0/0}
$fGenericVoid_$cto :: forall x. Rep Void x -> Void
$fGenericVoid_$cto
  = \ (@ x_a2HT) (ds_d2J8 :: Rep Void x_a2HT) ->
      case ds_d2J8 of { __DEFAULT -> $fGenericVoid1 }

That seems rather unfortunate. The only workaround I've found so far is to actually write a function just to constrain the type:

absV :: V1 r -> a
absV x = case x of

instance Generic Void where
  ...
  to = absV

Finally, this is clean:

-- RHS size: {terms: 5, types: 12, coercions: 0, joins: 0/0}
absV :: forall r a. V1 r -> a
absV
  = \ (@ r_a2Hy) (@ a_a2Hz) (x_a1fi :: V1 r_a2Hy) ->
      case x_a1fi of { }

-- RHS size: {terms: 4, types: 7, coercions: 0, joins: 0/0}
lvl_r2IF :: forall x. V1 x -> Void
lvl_r2IF = \ (@ x_a2HP) (eta_B1 :: V1 x_a2HP) -> absV eta_B1

I suppose I could add GHC.Generics.Absurd just to write the absV function for Generic and Generic1 deriving, but that seems more than a little silly.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture