skip constructor: substUnfolding

[lastland]

Issue by sweirich
Thursday Jun 27, 2019 at 18:27 GMT
Originally opened as antalsz/hs-to-coq#131

---

Processing this code fails when DFunUnfolding and CoreUnfolding constructors are skipped
(working around by redefining the function).

substUnfolding subst df@(DFunUnfolding { df_bndrs = bndrs, df_args = args })
  = df { df_bndrs = bndrs', df_args = args' }
  where
    (subst',bndrs') = substBndrs subst bndrs
    args'           = map (substExpr (text "subst-unf:dfun") subst') args

substUnfolding subst unf@(CoreUnfolding { uf_tmpl = tmpl, uf_src = src })
        -- Retain an InlineRule!
  | not (isStableSource src)  -- Zap an unstable unfolding, to save substitution work
  = NoUnfolding
  | otherwise                 -- But keep a stable one!
  = seqExpr new_tmpl `seq`
    unf { uf_tmpl = new_tmpl }
  where
    new_tmpl = substExpr (text "subst-unf") subst tmpl

substUnfolding _ unf = unf      -- NoUnfolding, OtherCon

The error message is

invalid record update with non-record-fields `Core.df_args' and `Core.df_bndrs' unsupported [in definition CoreSubst.substUnfolding in module CoreSubst]