420b465 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix 'impossible' error with empty types

isEmpty shouldn't consider function types to be empty, just things which can be deconstructed by pattern matching. Fixes #3614

commit420b465356e7fe8d9a11576e0d9641326ada3675 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Mar 2017, 22:37 (10 years ago) parente0cc0cf

1 file changed+2−2

unifiedsplit

src/Idris/Elab/Utils.hs+2−2

@@ -545,11 +545,11 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

545545

546546isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool

547547isEmpty ctxt tyctxt ty

548− | (P _ tyname _, args) <- unApply (getRetTy ty),

548+ | (P _ tyname _, args) <- unApply ty,

549549 Just tyinfo <- lookupCtxtExact tyname tyctxt

550550 -- Compare all the constructor types against the type we need

551551 -- If they *all* have an argument position where some constructor

552− -- clases with the needed type, then the type we're looking for must

552+ -- clashes with the needed type, then the type we're looking for must

553553 -- be empty

554554 = let neededty = getRetTy ty

555555 contys = mapMaybe getConType (con_names tyinfo) in