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