WARNING from typecorrect file

[sweirich]

WARNING: file compiler/coreSyn/CoreUtils.hs, line 245 Trying to coerce (se_amlB :: Sing b_amBc) Sub (TFCo:R:SingExpre[0] _N _N) Sing b_amBL ~R# R:SingExpre Nat b_amBL

File is wg28.hs (currently committed version) and the warining is from this code at the end of the file.

lemma :: Sing n -> (n :+ 'Zero) :~: n lemma SZero = Refl lemma (SSucc x) = case lemma x of Refl -> Refl

sOpt :: Sing e -> Equivalent e sOpt (SVal x) = Result (SVal x) Refl sOpt (SPlus (SVal SZero) se) = case sOpt se of Result se' Refl -> Result se' Refl sOpt (SPlus se (SVal SZero)) = case (sOpt se) of (Result se' Refl) -> case lemma (sEval se') of Refl -> Result se' Refl

-- sOpt (SPlus e0 e1) = case (sOpt e0, sOpt e1) of -- (Result e0' Refl, Result e1' Refl) -> Result (SPlus e0' e1') Refl

sOpt (SCond e0 e1 e2) = case (sOpt e0, sOpt e1, sOpt e2) of (Result e0' Refl, Result e1' Refl, Result e2' Refl) -> Result (SCond e0' e1' e2') Refl

[goldfirere]

This one looks nasty. Given that it's a warning, I'll wait until after imposing deadlines.

But the warning means that -dcore-lint will fail.