@@ -448,13 +448,12 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
448448 | otherwise = checkSize a ps
449449 checkSize a [] = Nothing
450450
451− -- the smaller thing we find must be defined in the same group of mutally
452− -- defined types as <a>, and not be coinductive - so carry the type of
453− -- the constructor we've gone under.
454−
455− smaller (Just tyn) a (t, Just tyt)
456− | a == t = isInductive (fst (unApply (getRetTy tyn)))
457− (fst (unApply (getRetTy tyt)))
451+ -- Can't be smaller than an erased thing (need to be careful here
452+ -- because Erased equals everything)
453+ smaller _ _ (Erased, _) = False -- never smaller than an erased thing
454+ -- If a == t, and we're under a cosntructor, we've found something
455+ -- smaller
456+ smaller (Just tyn) a (t, Just tyt) | a == t = True
458457 smaller ty a (ap@(App _ f s), _)
459458 -- Nothing can be smaller than a delayed infinite thing...
460459 | (P (DCon _ _ _) (UN d) _, [P _ (UN reason) _, _, _]) <- unApply ap,
@@ -473,13 +472,6 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
473472 getType n = case lookupTyExact n (tt_ctxt ist) of
474473 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
475474
476− isInductive (P _ nty _) (P _ nty' _) =
477− let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
478− [TI _ x _ _ muts _] -> (x, muts)
479− _ -> (False, []) in
480− (nty == nty' || any (== nty') muts) && not co
481− isInductive _ _ = False
482−
483475 dePat (Bind x (PVar _ ty) sc) = dePat (instantiate (P Bound x ty) sc)
484476 dePat t = t
485477