Issue with compiling pattern guards.

[sweirich]

With this definition from SmallStep.hs

exprIsTrivial' :: CoreExpr -> Bool
exprIsTrivial' (Tick _ e)               = exprIsTrivial' e
exprIsTrivial' (App e a) | isTypeArg a  = exprIsTrivial' e
exprIsTrivial' (Lam v e) | not (isId v) = exprIsTrivial' e
exprIsTrivial' (Cast e _)               = exprIsTrivial' e

exprIsTrivial' (Var _)      = True
exprIsTrivial' (Lit _)      = True
exprIsTrivial' (Coercion _) = True
exprIsTrivial' _ = False

I am getting this erroneous output (note toplevel match does not have the catchall branch):

Definition exprIsTrivial' : CoreSyn.CoreExpr -> bool :=
  fix exprIsTrivial' arg_0__
        := let j_2__ :=
             match arg_0__ with
             | CoreSyn.Cast e _ => exprIsTrivial' e
             | CoreSyn.Var _ => true
             | CoreSyn.Lit _ => true
             | CoreSyn.Coercion _ => true
             | _ => false
             end in
           match arg_0__ with
           | CoreSyn.Tick _ e => exprIsTrivial' e
           | CoreSyn.App e a =>
               if CoreSyn.isTypeArg a : bool then exprIsTrivial' e else
               j_2__
           | CoreSyn.Lam v e =>
               if negb (Var.isId v) : bool then exprIsTrivial' e else
               j_2__
           end.

[sweirich]

Maybe this is the problem:

When looking up information about CoreSyn.Cast in constructorTypes
Could not find CoreSyn.h2ci in any of these directories:
Please either process CoreSyn first, or
skip declarations that mention CoreSyn.

where do I tell hs-to-coq where to look for h2ci files?

[sweirich]

Yep, that was it.