collapseCons :: Name -> [(Name, Type)] -> Idris ()
collapseCons ty cons = 
     do i <- getIState
        let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
        allFR <- mapM (forceRec i) cons'
        if and allFR then detaggable (map getRetTy (map snd cons))
                     else return () -- not collapsible as not detaggable
  where
    setCollapsible :: Name -> Idris ()
    setCollapsible n
       = do i <- getIState
            iLOG $ show n ++ " collapsible"
            case lookupCtxt n (idris_optimisation i) of
               (oi:_) -> do let oi' = oi { collapsible = True }
                            let opts = addDef n oi' (idris_optimisation i)
                            putIState (i { idris_optimisation = opts })
               [] -> do let oi = Optimise True [] []
                        let opts = addDef n oi (idris_optimisation i)
                        putIState (i { idris_optimisation = opts })
                        addIBC (IBCOpt n)

    forceRec :: IState -> (Name, [Type]) -> Idris Bool
    forceRec i (n, ts)
       = case lookupCtxt n (idris_optimisation i) of
            (oi:_) -> checkFR (forceable oi) 0 ts
            _ -> return False
    checkFR fs i [] = return True
    checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
    checkFR fs i (t : xs)
        -- must be recursive or type is not collapsible
        = do let (rtf, rta) = unApply $ getRetTy t
             if (ty `elem` freeNames rtf) 
               then checkFR fs (i+1) xs
               else return False

    detaggable :: [Type] -> Idris ()
    detaggable rtys 
        = do let rtyArgs = map (snd . unApply) rtys
             -- if every rtyArgs is disjoint with every other, it's detaggable,
             -- therefore also collapsible given forceable/recursive check
             if disjoint rtyArgs
                then mapM_ setCollapsible (ty : map fst cons)
                else return ()

    disjoint :: [[Term]] -> Bool
    disjoint []       = True
    disjoint [x]      = True
    disjoint (x : xs) = anyDisjoint x xs && disjoint xs

    anyDisjoint x [] = True
    anyDisjoint x (y : ys) = disjointCons x y

    disjointCons [] [] = False
    disjointCons [] y  = False
    disjointCons x  [] = False
    disjointCons (x : xs) (y : ys)
        = disjointCon x y || disjointCons xs ys

    disjointCon x y = let (cx, _) = unApply x
                          (cy, _) = unApply y in
                          case (cx, cy) of
                               (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
                               _ -> False
collapseCons :: Name -> [(Name, Type)] -> Idris ()
collapseCons ty cons = 
     do i <- getIState
        let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
        allFR <- mapM (forceRec i) cons'
        if and allFR then detaggable (map getRetTy (map snd cons))
                     else return () -- not collapsible as not detaggable
  where
    setCollapsible :: Name -> Idris ()
    setCollapsible n
       = do i <- getIState
            iLOG $ show n ++ " collapsible"
            case lookupCtxt n (idris_optimisation i) of
               (oi:_) -> do let oi' = oi { collapsible = True }
                            let opts = addDef n oi' (idris_optimisation i)
                            putIState (i { idris_optimisation = opts })
               [] -> do let oi = Optimise True [] []
                        let opts = addDef n oi (idris_optimisation i)
                        putIState (i { idris_optimisation = opts })
                        addIBC (IBCOpt n)

    forceRec :: IState -> (Name, [Type]) -> Idris Bool
    forceRec i (n, ts)
       = case lookupCtxt n (idris_optimisation i) of
            (oi:_) -> checkFR (forceable oi) 0 ts
            _ -> return False
    checkFR fs i [] = return True
    checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
    checkFR fs i (t : xs)
        -- must be recursive or type is not collapsible
        = do let (rtf, rta) = unApply $ getRetTy t
             if (ty `elem` freeNames rtf) 
               then checkFR fs (i+1) xs
               else return False

    detaggable :: [Type] -> Idris ()
    detaggable rtys 
        = do let rtyArgs = map (snd . unApply) rtys
             -- if every rtyArgs is disjoint with every other, it's detaggable,
             -- therefore also collapsible given forceable/recursive check
             if disjoint rtyArgs
                then mapM_ setCollapsible (ty : map fst cons)
                else return ()

    disjoint :: [[Term]] -> Bool
    disjoint []       = True
    disjoint [x]      = True
    disjoint (x : xs) = anyDisjoint x xs && disjoint xs

    anyDisjoint x [] = True
    anyDisjoint x (y : ys) = disjointCons x y

    disjointCons [] [] = False
    disjointCons [] y  = False
    disjointCons x  [] = False
    disjointCons (x : xs) (y : ys)
        = disjointCon x y || disjointCons xs ys

    disjointCon x y = let (cx, _) = unApply x
                          (cy, _) = unApply y in
                          case (cx, cy) of
                               (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
                               _ -> False
collapseCons ty cons = 
     do i <- getIState
        let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons
        allFR <- mapM (forceRec i) cons'
        if and allFR then detaggable (map getRetTy (map snd cons))
                     else return () -- not collapsible as not detaggable
  where
    setCollapsible :: Name -> Idris ()
    setCollapsible n
       = do i <- getIState
            iLOG $ show n ++ " collapsible"
            case lookupCtxt n (idris_optimisation i) of
               (oi:_) -> do let oi' = oi { collapsible = True }
                            let opts = addDef n oi' (idris_optimisation i)
                            putIState (i { idris_optimisation = opts })
               [] -> do let oi = Optimise True [] []
                        let opts = addDef n oi (idris_optimisation i)
                        putIState (i { idris_optimisation = opts })
                        addIBC (IBCOpt n)

    forceRec :: IState -> (Name, [Type]) -> Idris Bool
    forceRec i (n, ts)
       = case lookupCtxt n (idris_optimisation i) of
            (oi:_) -> checkFR (forceable oi) 0 ts
            _ -> return False
    checkFR fs i [] = return True
    checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs
    checkFR fs i (t : xs)
        -- must be recursive or type is not collapsible
        = do let (rtf, rta) = unApply $ getRetTy t
             if (ty `elem` freeNames rtf) 
               then checkFR fs (i+1) xs
               else return False

    detaggable :: [Type] -> Idris ()
    detaggable rtys 
        = do let rtyArgs = map (snd . unApply) rtys
             -- if every rtyArgs is disjoint with every other, it's detaggable,
             -- therefore also collapsible given forceable/recursive check
             if disjoint rtyArgs
                then mapM_ setCollapsible (ty : map fst cons)
                else return ()

    disjoint :: [[Term]] -> Bool
    disjoint []       = True
    disjoint [x]      = True
    disjoint (x : xs) = anyDisjoint x xs && disjoint xs

    anyDisjoint x [] = True
    anyDisjoint x (y : ys) = disjointCons x y

    disjointCons [] [] = False
    disjointCons [] y  = False
    disjointCons x  [] = False
    disjointCons (x : xs) (y : ys)
        = disjointCon x y || disjointCons xs ys

    disjointCon x y = let (cx, _) = unApply x
                          (cy, _) = unApply y in
                          case (cx, cy) of
                               (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny
                               _ -> False