30f3a8b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

(Temporarily) remove the remaining typecase checks.

6e1cac72fd0660cd26beb6bb1f7ed5a1b65ec9bd temporarily disables the typecase test, but some checks remain and continue to cause undesired behaviour. This patch temporarily disables the remaining checks.

commit30f3a8b2a946dbc4bb58a627f08d81ab4f0dea6e authorSimon Fowler <sf37@st-andrews.ac.uk> dateMon 3 Feb 2014, 11:12 (13 years ago) parent5080735

1 file changed+6−6

compare with master

unifiedsplit

src/Idris/ElabTerm.hs+6−6

src/Idris/ElabTerm.hs+6−6

@@ -162,9 +162,9 @@ elab ist info pattern opts fn tm

162162

163163 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

164164 elab' ina PType = do apply RType []; solve

165− elab' (_,_,inty) (PConstant c)

166− | constType c && pattern && not reflect && not inty

167− = lift $ tfail (Msg "Typecase is not allowed")

165+-- elab' (_,_,inty) (PConstant c)

166+-- | constType c && pattern && not reflect && not inty

167+-- = lift $ tfail (Msg "Typecase is not allowed")

168168 elab' ina (PConstant c) = do apply (RConstant c) []; solve

169169 elab' ina (PQuote r) = do fill r; solve

170170 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

@@ -240,9 +240,9 @@ elab ist info pattern opts fn tm

240240 trySeq' deferr (x : xs)

241241 = try' (elab' ina x) (trySeq' deferr xs) True

242242 elab' ina (PPatvar fc n) | pattern = patvar n

243− elab' (_, _, inty) (PRef fc f)

244− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

245− = lift $ tfail (Msg "Typecase is not allowed")

243+-- elab' (_, _, inty) (PRef fc f)

244+-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

245+-- = lift $ tfail (Msg "Typecase is not allowed")

246246 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)

247247 = do ctxt <- get_context

248248 let defined = case lookupTy n ctxt of