PCase17.stderr

PCase17.hs:(18,14)-(24,7): Splicing expression
    ghc-internal:GHC.Internal.TH.Quote.quoteExp
      pCase
      " e of\n\
      \       Zero      -> e .== e =: qed\n\
      \       Num _     -> e .== e =: qed\n\
      \       Var _     -> e .== e =: qed\n\
      \       Add _ _   -> e .== e =: qed\n\
      \       Let _ _ _ -> e .== e =: qed\n\
      \     "
  ======>
    cases
      [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
       (isVar e ==> (e .== e =: qed)), (isAdd e ==> (e .== e =: qed)),
       (isLet e ==> (e .== e =: qed))]
PCase17.hs:18:14: error: [GHC-83865]
    " Couldn't match expected type: Proof SBool
                  with actual type: sbv-14.2:Data.SBV.TP.TP.TPProofGen
                                      (SBV Bool) [sbv-14.2:Data.SBV.TP.TP.Helper] ()
    " In the expression:
        cases
          [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
           (isVar e ==> (e .== e =: qed)), ....]
      In an equation for t:
          t e
            = (cases
                 [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
                  (isVar e ==> (e .== e =: qed)), ....])
   |
18 | t e = [pCase| e of
   |              ^^^^^...