Case reduction failure with GADT

[conal]

Case reduction fails in the following example (with a GADT):

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

{-# OPTIONS_GHC -Wall #-}

{-

  bash-3.2$ hermit CaseReduceGADT.hs -v0
  [starting HERMIT v0.4.0.0 on CaseReduceGADT.hs]
  % ghc CaseReduceGADT.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fexpose-all-unfoldings -fplugin=HERMIT -fplugin-opt=HERMIT:-v0 -fplugin-opt=HERMIT:*: -v0
  module main:CaseReduceGADT where
    headV ∷ ∀ n . Vec (S n) Int → Int
    bar ∷ Int
  hermit<0> rhs-of bar
  headV ▲ ($W:< ▲ ▲ (I# 10) ($WZVec ▲))
  hermit<1> set-pp-type Show
  headV Z ($W:< Int Z (I# 10) ($WZVec Int))
  hermit<1> unfold
  case $W:< Int Z (I# 10) ($WZVec Int) of wild Int
    _ → (λ ds → patError Int ("CaseReduceGADT.hs:39:1-18|function headV"#)) void#
    (:<) n □ x ds → x
  hermit<2> case-reduce
  Error in expression: case-reduce
  Rewrite failed: user error (Unsuitable expression for Case reduction.)
  hermit<2> case-reduce-datacon
  Error in expression: case-reduce-datacon
  Rewrite failed: user error (Case reduction failed: head of scrutinee is not a data constructor.)

-}

module CaseReduceGADT where

infixr 5 :<

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

headV :: Vec (S n) Int -> Int
headV (x :< _) = x

bar :: Int
bar = headV (10 :< ZVec)

[xich]

The scrutinee of the case ($W:< Int Z (I# 10) ($WZVec Int)) is a function application. If you:

hermit<2> down
$W:< Int Z (I# 10) ($WZVec Int)
hermit<3> unfold
(:<) (S Z) Int Z ■ (I# 10) ($WZVec Int)
hermit<4> up
case (:<) (S Z) Int Z ■ (I# 10) ($WZVec Int) of wild Int
  _ → (λ ds → patError Int ("GADT.hs:41:1-18|function headV"#)) void#
  (:<) n □ x ds → x
hermit<5> case-reduce
I# 10

Things work. We have a case-reduce-id command that inlines a scrutinee that is a single identifier, so I just added a case-reduce-unfold equivalent in 2ea8edbb6d52fd9f726dee62257daeef0a2d687a. (Really, case-reduce-unfold subsumes case-reduce-id, but the latter is used in some scripts, so I won't remove it just now.)

[conal]

Oh! Got it. Thanks a bunch.

[conal]

I see that caseReduceFoldR takes a flag saying whether to substitute (vs build a let). If subst is True, might we get replicated non-trivial computation? What are the trade-offs?

[Sculthorpen]

I agree, case-reduce-unfold does subsume case-reduce-id. The only place I was using it was in bash and smash, so I've now replaced that usage with case-reduce-unfold, and removed case-reduce-id entirely.