content: {-# LANGUAGE ImplicitParams #-}
  {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
  
  
  {-# options_ghc -fno-warn-incomplete-uni-patterns #-}
  module Language.Granule.Synthesis.SynthLinearBase where
  
  import Language.Granule.Syntax.Expr
  import Language.Granule.Syntax.Type
  import Language.Granule.Syntax.Identifiers
  import Language.Granule.Syntax.Pretty
  import Language.Granule.Syntax.Pattern
  import Language.Granule.Context
  import Language.Granule.Checker.Monad
  import Language.Granule.Checker.Predicates
  import Language.Granule.Checker.Kinding
  import Language.Granule.Checker.Substitution
  import Language.Granule.Checker.SubstitutionContexts
  import Language.Granule.Checker.Types
  import Language.Granule.Synthesis.Builders
  import Language.Granule.Synthesis.Monad
  import Language.Granule.Synthesis.Contexts
  import Language.Granule.Synthesis.Common
  import Language.Granule.Utils
  
  import Control.Monad.State.Strict
  import qualified System.Clock as Clock
  import Data.List (sortBy)
  
  
  -- Note that the way this is used, the (var, assumption) pair in the first
  -- argument is not contained in the provided context (second argument)
  useVar :: (?globals :: Globals)
    => (Id, SAssumption)
    -> Ctxt SAssumption
    -> ResourceScheme PruningScheme
    -> Maybe Type -- Grade-on-rule mode
    -> Synthesiser (Ctxt SAssumption)
  
  -- Subtractive
  useVar (name, SVar (Linear t) _ _) gamma Subtractive _ = return gamma
  useVar (name, SVar (Discharged t grade) sInfo depth) gamma Subtractive Nothing = do
    (kind, _, _) <- conv $ synthKind nullSpan grade
    var <- freshIdentifier
    conv $ existentialTopLevel var kind -- Existentials must be at the topLevel because they may be generated inside an implication but may occur outside of the implication
    st <- conv get
    -- modifyPred st $ addConstraintViaConjunction (ApproximatedBy ns (TyInfix TyOpPlus (TyVar var) (TyGrade (Just kind) 1)) grade kind) (predicateContext st)
    res <- solve
    boolToSynthesiser res (replace gamma name (SVar (Discharged t (TyVar var)) sInfo depth))
  
  --Subtractive Grade-on-Rule
  useVar (name, SVar (Discharged t grade) sInfo depth) gamma Subtractive (Just gradeOnRule) = do
    (kind, _, _) <- conv $ synthKind nullSpan grade
    var <- freshIdentifier
    conv $ existentialTopLevel var kind
    st <- conv get
    -- modifyPred st $ addConstraintViaConjunction (ApproximatedBy ns (TyInfix TyOpPlus (TyVar var) gradeOnRule) grade kind) (predicateContext st)
    res <- solve
    boolToSynthesiser res (replace gamma name (SVar (Discharged t (TyVar var)) sInfo depth))
  
  -- Additive
  useVar (name, SVar (Linear t) sInfo depth) _ Additive{} _ = return [(name, SVar (Linear t) sInfo depth)]
  useVar (name, SVar (Discharged t grade) sInfo depth) _ Additive{} Nothing = do
    (kind, _, _) <- conv $ synthKind nullSpan grade
    return [(name, SVar (Discharged t (TyGrade (Just kind) 1)) sInfo depth)]
  useVar (name, SVar (Discharged t grade) sInfo depth) _ Additive{} (Just gradeOnRule) = do
    (kind, _, _) <- conv $ synthKind nullSpan grade
    return [(name, SVar (Discharged t gradeOnRule) sInfo depth)]
  
  -- Defs
  -- For top level definitions we do not need to track resource usage
  useVar (name, def@SDef{}) gamma Subtractive _ = return ((name, def):gamma)
  useVar (name, def@SDef{}) _ Additive{} _ = return []
  
  
  {--
  Subtractive
  
  ------------------------ :: lin_var
  Γ, x : A ⊢ A ⇒ x ; Γ
  
        ∃s. s + 1 = r
  ------------------------ :: gr_var
  Γ, x : [A] r ⊢ A ⇒ x ; Γ, x : [A] s
  
  Additive
  
  ------------------------ :: lin_var
  Γ, x : A ⊢ A ⇒ x ; x : A
  
  ------------------------ :: gr_var
  Γ, x : [A] r ⊢ A ⇒ x ; x : [A] 1
  
  --}
  varHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> FocusedCtxt SAssumption
    -> FocusedCtxt SAssumption
    -> ResourceScheme PruningScheme
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  varHelper _ _ (Focused []) _ _ _ = none
  varHelper gamma (Focused left) (Focused (var@(id, assumption) : right)) resourceScheme grade goal@(Goal (goalTySch@(Forall _ _ _ goalTy)) _) =
    varHelper gamma (Focused (var:left)) (Focused right) resourceScheme grade goal `try` do
      -- debugM "synthDebug - inside varHelper checking var: " (show var <> " against goal " <> show goalTy)
      case assumption of
        SVar a sInfo _ -> do
          conv $ resetAddedConstraintsFlag -- reset the flag that says if any constraints were added
          (success, specTy, subst) <- conv $ equalTypes ns (getAssumptionType a) goalTy
  
          cs <- conv $ get
          -- Take the constraints generated by the type equality and add these to the synthesis predicate
          -- modifyPred cs $ addPredicateViaConjunction (Conj $ predicateStack cs) (predicateContext cs)
  
          -- Clear the checker state predicate
          conv $ modify (\s -> s { predicateStack = []})
  
          if success then do
            -- see if any constraints were added
            solved <- if addedConstraints cs
                    then solve
                    else return True
            -- now to do check we can actually use it
            if solved then do
              delta <- useVar var (gamma ++ (left ++ right)) resourceScheme grade
              return (Val ns goalTy False (Var goalTy id), delta, subst, [], isDecr sInfo)
            else none
          else none
        SDef t g _ -> do
          -- Using a top level definition as a variable
          undefined
  
  
  
  
  
  {--
  Subtractive
  
  x ∉ Δ
  Γ, x : A ⊢ B ⇒ t ; Δ
  ------------------------ :: abs
  Γ ⊢ A → B ⇒ λx . t ; Δ
  
  Additive
  
  Γ, x : A ⊢ B ⇒ t ; Δ, x : A
  ------------------------ :: abs
  Γ ⊢ A → B ⇒ λx . t ; Δ
  
  --}
  absHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> FocusedCtxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  absHelper gamma (Focused omega) resourceScheme inDef depth focusPhase grade goal@(Goal goalTySch@(Forall _ binders constraints gt@(FunTy name _ tyA tyB)) sInf) = do
  
    -- Fresh var
    id <- useBinderNameOrFreshen name
  
    -- Build recursive context depending on focus mode
    let (gamma', omega') = bindToContext (id, SVar (Linear tyA) (Just $ NonDecreasing 0) 0) gamma omega (isLAsync tyA)
  
    debugM "synthDebug" $ "(abs) lambda-binding " ++ pretty [(id, Linear tyA)]
  
    -- Synthesise body
    (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner resourceScheme inDef depth focusPhase gamma' (Focused omega') grade (Goal (Forall ns binders constraints tyB) sInf)
  
    -- Check resource use at the end
    case (resourceScheme, lookupAndCutout id delta) of
      (Additive{}, Just (delta', SVar (Linear _) _ _)) -> do
        return (Val ns gt False (Abs gt (PVar ns tyA False id) Nothing e), delta', subst, bindings, structurallyDecr)
      (Subtractive, Nothing) ->
        return (Val ns gt False (Abs gt (PVar ns tyA False id) Nothing e), delta, subst, bindings, structurallyDecr)
      _ -> none
  absHelper _ _ _ _ _ _ _ _ = none
  
  
  appHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> FocusedCtxt SAssumption
    -> FocusedCtxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  appHelper _ _ (Focused []) _ _ _ _ _ _ = none
  {-
  Subtractive
  
  x2 ∉ Δ1
  Γ, x2 : B ⊢ C ⇒ t1 ; Δ1
  Δ1 ⊢ A ⇒ t2 ; Δ2
  ------------------------ :: app
  Γ, x1 : A → B ⊢ C ⇒ [(x1 t2) / x2] t1 ; Δ2
  
  -}
  appHelper gamma (Focused left) (Focused (var@(x, assumption) : right)) Subtractive inDef depth focusPhase grade goal@(Goal goalTySch@(Forall _ binders constraints gt) _) =
    appHelper gamma (Focused (var : left)) (Focused right) Subtractive inDef depth focusPhase grade goal `try` do
    assumptionTy <- getSAssumptionType assumption
    (case assumptionTy of
      (FunTy _ _ tyA tyB, isTopLevelDef, _, _, _, _) -> do
  
        -- Only try the app if we haven't hit the app allowed depth
        -- debugM "synthDebug - (app) trying to use a function " (show var ++ " to get goal " ++ pretty goalTySch)
  
        let omega = left ++ right
  
        leftOver <- useVar var omega Subtractive grade
  
        y <- freshIdentifier
  
        -- We need to move the assumption we have just used out of the focusing context and back into gamma
        let (gamma', omega') =
                case lookupAndCutout x leftOver of
                  Just (omega'', var') -> (gamma ++ [(x, var')], omega'')
                  _ -> (gamma, leftOver)
  
            -- Extend context (focused) with x2 : B
        let (gamma'', omega'') = bindToContext (y, SVar (Linear tyB) Nothing 0) gamma' omega' (isLAsync tyB)
  
        -- debugM "synthDebug - (app) try to synth the goal " (pretty goalTySch ++ "\n under context of gamma'': " ++ (show gamma'') ++ "\n , omega'': " ++ (show omega''))
        (e1, delta1, subst1, bindings1, structurallyDecr1) <- synthesiseInner Subtractive inDef depth focusPhase gamma'' (Focused omega'') grade goal
        case lookup y delta1 of
          Nothing -> do
            debugM "synthDebug - (app) try to synth the argument at type "  (pretty tyA)
  
            -- Synthesise the argument
            (e2, delta2, subst2, bindings2, structurallyDecr2) <- synthesiseInner Subtractive inDef depth RightSync delta1 (Focused []) grade (Goal (Forall ns binders constraints tyA) $ Just $ NonDecreasing 0)
            state <- getSynthState
  
            -- If this is an application of the top level def we are currently defining, then ensure the result is structurally recursive
            if not isTopLevelDef || structurallyDecr1 || structurallyDecr2 || not (x `elem` currDef state) then do
              substOut <- conv $ combineSubstitutions ns subst1 subst2
              let appExpr = App ns gt False (Val ns tyA False (Var tyA x)) e2
              return (Language.Granule.Syntax.Expr.subst appExpr y e1, delta2, substOut, bindings1 ++ bindings2, structurallyDecr1 || structurallyDecr2)
            else none
          _ -> none
      _ -> none)
  {-
  Additive
  
  Γ, x2 : B ⊢ C ⇒ t1 ; Δ1, x2 : B
  Γ ⊢ A ⇒ t2 ; Δ2
  ------------------------ :: app
  Γ, x1 : A → B ⊢ C ⇒ [(x1 t2) / x2] t1 ; (Δ1 + Δ2), x1: A → B
  
  Additive (Pruning)
  
  Γ, x2 : B ⊢ C ⇒ t1 ; Δ1, x2 : B
  Γ - Δ1 ⊢ A ⇒ t2 ; Δ2
  ------------------------ :: app
  Γ, x1 : A → B ⊢ C ⇒ [(x1 t2) / x2] t1 ; (Δ1 + Δ2), x1: A → B
  
  -}
  appHelper gamma (Focused left) (Focused (var@(x, assumption) : right)) add@(Additive mode) inDef depth focusPhase grade goal@(Goal goalTySch@(Forall _ binders constraints gt) _) =
    appHelper gamma (Focused (var : left)) (Focused right) add inDef depth focusPhase grade goal `try` do
    assumptionTy <- getSAssumptionType assumption
    case assumptionTy of
      (FunTy _ _ tyA tyB, isTopLevelDef, _, _, _, _) -> do
  
        let omega = (left ++ right)
        used <- useVar var omega add grade
  
        y <- freshIdentifier
  
        -- Extend context (focused) with y : B
        let (gamma', omega') = bindToContext (y, SVar (Linear tyB) Nothing 0) (var:gamma) omega (isLAsync tyB)
  
          -- Synthesise the goal using the result of the application
        (e1, delta1, subst1, bindings1, structurallyDecr1) <- synthesiseInner add (inDef || isTopLevelDef) depth focusPhase gamma' (Focused omega') grade goal
  
        -- Make sure that `y` appears in the result
        case lookupAndCutout y delta1 of
          Just (delta1',  SVar (Linear _) _ _) -> do
            -- Pruning subtraction
            gamma2 <-
              case mode of
                NonPruning  -> return (omega ++ (var:gamma))
                Pruning -> ctxtSubtract (omega ++ (var:gamma)) delta1'
  
            -- Synthesise the argument
            (e2, delta2, subst2, bindings2, structurallyDecr2) <- synthesiseInner add (inDef || isTopLevelDef) depth RightSync gamma2 (Focused []) grade (Goal (Forall ns binders constraints tyA) $ Just $ NonDecreasing 0)
  
            st <- getSynthState
  
            -- If this is an application of the top level def we are currently defining, then ensure the result is structurally recursive
            if not isTopLevelDef || structurallyDecr1 || structurallyDecr2 || not (x `elem` currDef st) then  do
  
              -- Add the results
              deltaOut <- maybeToSynthesiser $ ctxtAdd used delta1'
              deltaOut' <- maybeToSynthesiser $ ctxtAdd deltaOut delta2
  
              substOut <- conv $ combineSubstitutions nullSpan subst1 subst2
              let appExpr = App ns gt False (Val ns tyA False (Var tyA x)) e2
              return (Language.Granule.Syntax.Expr.subst appExpr y e1, deltaOut', substOut, bindings1 ++ bindings2, (structurallyDecr1 || structurallyDecr2) || isTopLevelDef)
            else none
          _ -> none
      _ -> none
  
  
  {-
  Subtractive
  
  Γ ⊢ A ⇒ t ; Δ
  ------------------------ :: box
  Γ ⊢ [] r A ⇒ t ; Γ - r * (G - Δ)
  
  Additive
  
  Γ ⊢ A ⇒ t ; Δ
  ---------------------------- :: box
  Γ ⊢ [] r A ⇒ [t] ; r * Δ
  
  -}
  boxHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  boxHelper gamma resourceScheme inDef depth focusPhase grade (Goal goalTySch@(Forall _ binders constraints (Box g t)) _) =
    let newGradeOnRule = case grade of Just gradeOnRule -> Just $ TyInfix TyOpTimes gradeOnRule g ; Nothing -> Nothing
    in case resourceScheme of
        Additive{} -> do
          (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner resourceScheme inDef depth focusPhase gamma (Focused []) newGradeOnRule (Goal (Forall ns binders constraints t) $ Just $ NonDecreasing 0)
          case hasLinear delta of
            False -> do deltaOut <-
                          case newGradeOnRule of
                            Just _ -> return delta
                            Nothing -> ctxtMultByCoeffect g delta
                        let boxExpr = Val ns t False (Promote t e)
                        return (boxExpr, deltaOut, subst, bindings, structurallyDecr)
            True  -> none
        Subtractive -> do
          (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner resourceScheme inDef depth focusPhase gamma (Focused []) newGradeOnRule (Goal (Forall ns binders constraints t) $ Just $ NonDecreasing 0)
          deltaOut <- case newGradeOnRule of
              Just _ -> return delta
              Nothing -> do
                used <- ctxtSubtract gamma delta
                -- Compute what was used to synth e
                delta' <- ctxtMultByCoeffect g used
                ctxtSubtract gamma delta'
          res <- solve
          let boxExpr = Val ns t False (Promote t e)
          boolToSynthesiser res (boxExpr, deltaOut, subst, bindings, structurallyDecr)
  
    where
  
      hasLinear [] = False
      hasLinear ((x, SVar (Linear _) _ _):xs) = True
      hasLinear ((x, _):xs) = hasLinear xs
  
  boxHelper _ _ _ _ _ _ _ = none
  
  
  unboxHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> FocusedCtxt SAssumption
    -> FocusedCtxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  unboxHelper _ _ (Focused []) _ _ _ _ _ _ = none
  {-
  Subtractive
  0 <= s
  Γ, x2 : [A] r ⊢ B ⇒ e ; Δ, x2 : [A] s
  -------------------------------------------- :: unbox
  Γ, x1 : [] r A ⊢ B ⇒ let [x2] = x1 in e; Δ
  
  -}
  unboxHelper gamma (Focused left) (Focused (var@(x, assumption) : right)) Subtractive inDef depth focusPhase grade goal@(Goal goalTySch _) =
    unboxHelper gamma (Focused (var : left)) (Focused right) Subtractive inDef depth focusPhase grade goal `try` do
      assumptionTy <- getSAssumptionType assumption
      case assumptionTy of
        ((Box grade_r tyA), False, Nothing, sInfo, _, _) -> do
  
          -- debugM "synthDebug" $ "Trying to unbox " ++ show assumption
  
          let omega = left ++ right
          leftOver <- useVar var omega Subtractive grade
          y <- freshIdentifier
          let (gamma', omega') = bindToContext (y, SVar (Discharged tyA grade_r) sInfo 0) gamma leftOver (isLAsync tyA)
          -- debugM "synthDebug" $ "Inside unboxing try to synth for " ++ pretty goalTySch ++ " under " ++ pretty [(y, Discharged tyA grade_r)]
  
          (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner Subtractive inDef depth focusPhase gamma' (Focused omega') grade goal
          case lookupAndCutout y delta of
            Just (delta', SVar (Discharged _ grade_s) _ _) -> do
              -- Check that: 0 <= s
              (kind, _, _) <- conv $ synthKind nullSpan grade_s
              s <- conv get
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) grade_s kind) (predicateContext s)
              res <- solve
  
              -- If we succeed, create the let binding
              boolToSynthesiser res (makeUnbox y x goalTySch (Box grade_r tyA) tyA e, delta', subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
            _ -> none
        ((Box grade_r tyA), False, Just grade_s, Just sInfo, _, _) -> do
          debugM "synthDebug - (unbox - double) trying a double unboxing with "  (show grade_r)
  
          let omega = left ++ right
          leftOver <- useVar var [] Subtractive grade
          y <- freshIdentifier
          let (gamma', omega') = bindToContext (y, SVar (Discharged tyA (TyInfix TyOpTimes grade_r grade_s)) (Just sInfo) 0) gamma omega (isLAsync tyA)
          (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner Subtractive inDef depth focusPhase gamma' (Focused omega') grade goal
          case lookupAndCutout y delta of
            Just (delta', SVar (Discharged _ grade_s') _ _) ->  do
              (kind, _, _) <- conv $ synthKind nullSpan grade_s'
              r' <- freshIdentifier
              conv $ existentialTopLevel r' kind
              s <- conv get
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyInfix TyOpTimes (TyVar r') grade_s) grade_s' kind) (predicateContext s)
              res <- solve
              debugM "synthDebug - (unbox - double) term: " (pretty $ makeUnbox y x goalTySch (Box grade_r tyA) tyA e)
              boolToSynthesiser res (makeUnbox y x goalTySch (Box grade_r tyA) tyA e, replace delta' x (SVar (Discharged (Box grade_r tyA) (TyVar r')) (Just sInfo) 0), subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
            _ -> none
        _ -> none
  {-
  Additive
  
  s <= r
  Γ, x2 : [A] r ⊢ B ⇒ t ; D, x2 : [A] s
  --------------------------------------------------------- :: unbox
  Γ, x1 : [] r A ⊢ B ⇒ let [x2] = x1 in t ; Δ, x1 : [] r A
  
  -}
  unboxHelper gamma (Focused left) (Focused (var@(x, ty) : right)) add@(Additive{}) inDef depth focusPhase grade goal@(Goal goalTySch _) =
    unboxHelper gamma (Focused (var : left)) (Focused right) add inDef depth focusPhase grade goal `try`
    case ty of
      (SVar (Linear (Box grade_r tyA)) sInfo _) -> do
        let omega = left ++ right
        used <- useVar var omega add grade
        y <- freshIdentifier
  
        let (gamma', omega') = bindToContext (y, SVar (Discharged tyA grade_r) sInfo 0) gamma omega (isLAsync tyA)
  
        -- Synthesise the body of a `let` unboxing
        (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner add inDef depth focusPhase gamma' (Focused omega') grade goal
  
        -- Add usage at the binder to the usage in the body
        delta' <- maybeToSynthesiser $ ctxtAdd used delta
  
        s <- conv get
  
        case lookupAndCutout y delta' of
          Just (delta'', SVar (Discharged _ grade_s) _ _) -> do
            (kind, _, _) <- conv $ synthKind nullSpan grade_r
            -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns grade_s grade_r kind) (predicateContext s)
            res <- solve
            boolToSynthesiser res (makeUnbox y x goalTySch tyA (Box grade_r tyA) e,  delta'', subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
          _ -> do
            (kind, _, _) <- conv $ synthKind nullSpan grade_r
            -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) grade_r kind) (predicateContext s)
            res <- solve
            boolToSynthesiser res (makeUnbox y x goalTySch tyA (Box grade_r tyA) e,  delta', subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
      (SVar (Discharged (Box grade_r tyA) grade_s) sInfo _) -> do
        let omega = left ++ right
        used <- useVar var [] add grade
        y <- freshIdentifier
        let (gamma', omega') = bindToContext (y, SVar (Discharged tyA (TyInfix TyOpTimes grade_r grade_s)) sInfo 0) gamma omega (isLAsync tyA)
        (e, delta, subst, bindings, structurallyDecr) <- synthesiseInner add inDef depth focusPhase gamma' (Focused omega') grade goal
  
        s <- conv get
  
        case lookupAndCutout y delta of
          Just (delta', SVar (Discharged _ grade_s') _ depth) ->  do
            (kind, _, _) <- conv $ synthKind nullSpan grade_s'
            r' <- freshIdentifier
            conv $ existentialTopLevel r' kind
            s <- conv $ get
  
            -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyInfix TyOpTimes (TyVar r') grade_s) (TyInfix TyOpTimes grade_r grade_s) kind) (predicateContext s)
            -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyInfix TyOpTimes (TyVar r') grade_s) grade_s' kind) (predicateContext s)
  
            res <- solve
  
            boolToSynthesiser res (makeUnbox y x goalTySch (Box grade_r tyA) tyA e, replace delta x (SVar (Discharged (Box grade_r tyA) (TyVar r')) sInfo depth), subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
          _ -> do
              (kind, _, _) <- conv $ synthKind nullSpan grade_r
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) (TyInfix TyOpTimes grade_r grade_s) kind) (predicateContext s)
              res <- solve
              boolToSynthesiser res (makeUnbox y x goalTySch (Box grade_r tyA) tyA e, delta, subst, (x, (y, Box grade_r tyA)):bindings, structurallyDecr)
      _ -> none
  
  
  
  {--
  
  
  --}
  constrIntroHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  constrIntroHelper gamma resourceScheme False depth focusPhase grade goal@(Goal goalTySch@(Forall s binders constraints tyA) sInfo) = do
    case (isADTorGADT tyA) of
      Just name -> do
        if True || iCurrent depth <= intros depth || isDecr sInfo then do
  
          state <- getSynthState
          let (recursiveCons, nonRecursiveCons) = relevantConstructors name (constructors state)
          let sortedCons = sortBy compareArity nonRecursiveCons ++ sortBy compareArity recursiveCons
          -- traceM "here"
  
          -- For each relevent data constructor, we must now check that it's type matches the goal
          (maybeExpr, deltaOut, substOut, bindingsOut, structurallyDecrOut) <- tryConstructors name state [] sortedCons
          case maybeExpr of
            Just expr -> return (expr, deltaOut, substOut, bindingsOut, False)
            _ -> none
        else none
      _ -> none
    where
  
      tryConstructors _ _ _ [] = none
      tryConstructors adtName state right ((conName, (conTySch@(Forall s conBinders conConstraints conTy), conSubst)):left) =
        tryConstructors adtName state ((conName, (conTySch, conSubst)):right) left `try` do
          result <- checkConstructor conTySch tyA conSubst
          case result of
            (True, specTy, args, specSubst, substFromFreshening, predicate) -> do
              modifyPred (addPredicateViaConjunction predicate)
              specTy' <- conv $ substitute substFromFreshening specTy
              subst' <- conv $ combineSubstitutions s conSubst specSubst
              specTy'' <- conv $ substitute subst' specTy'
              case args of
                [] -> do
                  let delta = case resourceScheme of Additive{} -> [] ; Subtractive{} -> gamma
                  let conExpr = Val ns (TyCon conName) True (Constr (TyCon conName) conName [])
                  return (Just $ conExpr, delta, conSubst, [], False)
                conArgs@(_:_) -> do
                  args <- conv $ mapM (\(s,_) -> do
                    subst'' <- combineSubstitutions ns conSubst specSubst
                    s' <- substitute subst'' s
                    return (s', Just $ boolToStructure $ isDecreasing adtName [s'])) conArgs
                  (exprs, delta, subst, bindings, structurallyDecr) <- synthConArgs adtName (constructors state) args conBinders conConstraints conSubst
                  return (Just $ makeConstr exprs conName conTy, delta, subst, bindings, structurallyDecr)
            _ -> none
  
      -- constrArgs :: Type -> Maybe [Type]
      -- constrArgs (TyCon _) = Just []
      -- constrArgs (TyApp _ _) = Just []
      -- constrArgs (FunTy _ _ e1 e2) = do
      --   res <- constrArgs e2
      --   return $ e1 : res
      -- constrArgs _ = Nothing
  
      -- Traverse the argument types to the constructor and synthesise a term for each one
      synthConArgs tyAName consGlobal [(argTyA, sInfo)] conBinders conConstraints conSubst = do
        let newDepth = if isDecr sInfo then depth { iCurrent = (iCurrent depth) + 1 } else depth
        (expr, delta, subst, bindings, structurallyDecr) <- synthesiseInner resourceScheme False newDepth RightAsync gamma (Focused []) grade (Goal (Forall s conBinders conConstraints argTyA) sInfo)
        subst' <- conv $ combineSubstitutions ns conSubst subst
        return ([(expr, argTyA)], delta, subst', bindings, structurallyDecr)
      synthConArgs tyAName consGlobal ((argTyA, sInfo):args) conBinders conConstraints conSubst = do
        (exprs, deltas, substs, bindings, structurallyDecr) <- synthConArgs tyAName consGlobal args conBinders conConstraints conSubst
        substs' <- conv $ combineSubstitutions ns conSubst substs
        gamma' <- case resourceScheme of
              Additive NonPruning -> return gamma
              Additive Pruning -> ctxtSubtract gamma deltas -- Pruning
              Subtractive -> return deltas
        let newDepth = if isDecr sInfo then depth { iCurrent = (iCurrent depth) + 1 } else depth
        (expr, delta, subst, bindings', structurallyDecr') <- synthesiseInner resourceScheme False newDepth RightAsync gamma' (Focused []) grade (Goal (Forall s conBinders conConstraints argTyA) sInfo)
        subst'' <- conv $ combineSubstitutions ns subst substs'
        delta' <- case resourceScheme of
              Additive{} -> maybeToSynthesiser $ ctxtAdd deltas delta
              Subtractive -> return delta
        return ((expr, argTyA):exprs, delta', subst'', bindings ++ bindings', structurallyDecr || structurallyDecr')
      synthConArgs _ _ _ _ _ _ = none
  
      boolToStructure False = NonDecreasing 0
      boolToStructure True  = Decreasing 0
  
  constrIntroHelper _ _ _ _ _ _ _ = none
  
  
  
  
  
  {-
  
  Constructor elimination synthesis
  ---------------------------------
  
  
  -}
  constrElimHelper :: (?globals :: Globals)
    => Ctxt SAssumption
    -> FocusedCtxt SAssumption
    -> FocusedCtxt SAssumption
    -> ResourceScheme PruningScheme
    -> Bool
    -> Depth
    -> FocusPhase
    -> Maybe Type
    -> Goal
    -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  constrElimHelper _ _ (Focused []) _ _ _ _ _ _ = none
  constrElimHelper gamma (Focused left) (Focused (var@(x, assumption):right)) mode False depth focusPhase grade goal@(Goal goalTySch@(Forall _ _ _ tyB) _) =
    constrElimHelper gamma (Focused (var:left)) (Focused right) mode False depth focusPhase grade goal `try` do
      assumptionTy <- getSAssumptionType assumption
      case assumptionTy of
        (tyA', False, assumptionGrade, Just sInfo, _, _) -> do
          let (allowElim, currentDepth) = case sInfo of
                Decreasing eDepth -> (eDepth <= elims depth, eDepth)
                _ -> (True, 0)
          if allowElim then do
            -- debugM "synthDebug in constrElimHelper with assumption: " (show assumption <> " and goal " <> show tyB)
            case isADTorGADT tyA' of
              Just name -> do
                let omega = (left ++ right)
                usageOut <- useVar var omega mode grade
                state <- getSynthState
  
                let (recursiveCons, nonRecursiveCons) = relevantConstructors name (constructors state)
                let sortedCons = sortBy compareArity nonRecursiveCons ++ sortBy compareArity recursiveCons
  
                (patterns, delta, resSubst, resBindings, structurallyDecr, _) <- foldM (\ (exprs, deltas, substs, bindings, structurallyDecr, index) (conId, (conTySch@(Forall s binders constraints conTy), conSubst)) -> do
  
                  cs <- conv get
                  let pred = newImplication [] (predicateContext cs)
  
                  debugM "compiletoSBV ELIM (check constructor)" $ pretty conId
                  result <- checkConstructor conTySch tyA' conSubst
  
                  let predSucceeded = moveToConsequent pred
  
                  case (result, predSucceeded) of
                    ((True, specTy, conTyArgs, conSubst', _, _), Right pred'@(ImplConsequent ctxt p path)) -> do
  
                      -- modifyPred cs pred'
  
                      -- Calculate assumptions
                      assumptions <- mapM (\ (arg, _) -> do
                        y <- freshIdentifier
                        arg' <- conv $ substitute conSubst' arg
                        let assumptionType = case assumptionGrade of {Nothing -> Linear arg'; Just grade_r -> Discharged arg' grade_r}
                        let assumption = if isRecursiveCon name (y, (Forall ns binders constraints arg, []))
                            then (y, (SVar assumptionType (Just (Decreasing $ currentDepth+1)) 0))
                            else (y, (SVar assumptionType (Just $ NonDecreasing 0) 0))
                        return assumption) conTyArgs
  
                      let (vars, _) = unzip assumptions
                      let constrElimPattern = makePattern conId vars grade
  
  
                      -- If we are rebinding the assumption we are currently doing the eliminatino on (i.e. if it's graded) then
                      -- we need to rebing it in gamma NOT omega. Otherwise we will end up staying focused on it and trying to use
                      -- it even when we can not
  
                      (gamma', omega') <-
                        case mode of
                          Additive{} -> return (gamma, omega) --return (((x, (tyA, (AInfo structure (eDepth+1)))):gamma), omega)
                          Subtractive ->
                            case lookupAndCutout x usageOut of
                              Just (usageOut', assumption') -> return (gamma ++ [(x, assumption')], usageOut')
                              _ -> return (gamma, usageOut)
  
                      -- Required for focusing with recursive data structures. If we have hit the depth limit but still have other vars in omega
                      -- that cannot be decomposed we need to move them into gamma
  
                      let reachedDepth = currentDepth + 1 > elims depth
  
                      let (gamma'', omega'', unboxed) = bindAssumptions reachedDepth [] assumptions gamma' omega'
  
                      (expr, delta, subst, bindings, structurallyDecr') <- synthesiseInner mode False depth focusPhase gamma'' (Focused omega'') grade goal
  
                      delta' <- checkAssumptions (x, tyA') mode delta assumptions unboxed
  
                      case transformPattern bindings tyA' (gamma'' ++ omega'') constrElimPattern unboxed of
                        Just (pattern, bindings') ->
                          let mergeOp = case mode of Additive{} -> TyInfix TyOpJoin ; _ -> TyInfix TyOpMeet in do
                            returnDelta <- if index == 0 then return delta' else ctxtMergeFromPure mergeOp deltas delta'
                            -- modifyPred cs $ moveToNewConjunct (predicateContext cs)
                            returnSubst <- conv $ combineSubstitutions ns subst substs
                            return ((pattern, expr):exprs, returnDelta, returnSubst, bindings ++ bindings', structurallyDecr || structurallyDecr', index + 1)
                        Nothing -> do
                          -- modifyPred cs $ moveToNewConjunct (predicateContext cs)
                          return (exprs, deltas, substs, bindings, structurallyDecr, index)
                    _ -> do
                      -- modifyPred cs $ moveToNewConjunct (predicateContext cs)
                      return (exprs, deltas, substs, bindings, structurallyDecr, index)
                  ) ([], [], [], [], False, 0) sortedCons
                case patterns of
                  (_:_) -> do
                    finDelta <- case (mode, assumptionGrade) of {(Additive{}, Nothing) -> maybeToSynthesiser $ ctxtAdd usageOut delta; _ -> return delta}
                    return (makeCase tyA' x patterns tyB assumptionGrade, finDelta, resSubst, resBindings, structurallyDecr)
                  _ -> none
              _ -> none
          else none
        _ -> none
  
    where
  
    makePattern :: Id -> [Id] -> Maybe Type -> Pattern ()
    makePattern conId vars _ = PConstr ns () False conId [] (map (PVar ns () False) vars)
  
    bindAssumptions ::
      Bool
      -> Ctxt SAssumption
      -> Ctxt SAssumption
      -> Ctxt SAssumption
      -> Ctxt SAssumption
      -> (Ctxt SAssumption, Ctxt SAssumption, Ctxt SAssumption)
    bindAssumptions depthReached unboxed [] gamma omega = (gamma, omega, unboxed)
  
    bindAssumptions depthReached unboxed (assumption@(id, SVar (Linear t) sInfo depth):assmps) gamma omega =
      let gammaOrOmega = if depthReached && isDecr sInfo then False else isLAsync t in
      let (gamma', omega') = bindToContext assumption gamma omega gammaOrOmega in
      bindAssumptions depthReached unboxed assmps gamma' omega'
  
    bindAssumptions depthReached unboxed (assumption@(id, SVar (Discharged (Box t grade) grade') sInfo depth):assmps) gamma omega =
      let gammaOrOmega = if depthReached && isDecr sInfo then False else isLAsync t in
      let (gamma', omega') = bindToContext (id, SVar (Discharged t (TyInfix TyOpTimes grade grade')) sInfo depth) gamma omega gammaOrOmega in
      bindAssumptions depthReached ((id, SVar (Discharged t (TyInfix TyOpTimes grade grade')) sInfo depth):unboxed) assmps gamma' omega'
  
    bindAssumptions depthReached unboxed (assumption@(id, SVar (Discharged t _) sInfo depth):assmps) gamma omega =
      let gammaOrOmega = if depthReached && isDecr sInfo then False else isLAsync t in
      let (gamma', omega') = bindToContext assumption gamma omega gammaOrOmega in
      bindAssumptions depthReached unboxed assmps gamma' omega'
  
    bindAssumptions depthReached unboxed ((id, _):assmps) gamma omega = (gamma, omega, unboxed)
  
  
  
    -- Checks that assumptions bound via constrElim were used correctly in the synthesised term
    checkAssumptions :: (?globals::Globals)
      => (Id, Type)
      -> ResourceScheme PruningScheme
      -> Ctxt SAssumption
      -> Ctxt SAssumption
      -> Ctxt SAssumption
      -> Synthesiser (Ctxt SAssumption)
    checkAssumptions _ mode del [] _ = return del
    checkAssumptions x sub@Subtractive{} del ((id, SVar (Linear t) _ _):assmps) unboxed =
      case lookup id del of
        Nothing -> checkAssumptions x sub del assmps unboxed
        _ -> none
    checkAssumptions (x, t') sub@Subtractive{} del ((id, (SVar (Discharged t g) info depth)):assmps) unboxed = do
      s <- conv get
      case lookupAndCutout id del of
        Just (del', (SVar (Discharged _ g') sInfo _)) ->
          case lookup id unboxed of
            Just (SVar (Discharged _ g'') sInfo' _) -> do
              del'' <- checkAssumptions (x, t') sub del' assmps unboxed
              (kind, _, _) <- conv $ synthKind nullSpan g'
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) g' kind) (predicateContext s)
              res <- solve
              if res then do
                ctxtMergeFromPure (TyInfix TyOpMeet) [(x, (SVar (Discharged t' g) sInfo depth))] del''
              else none
            _ -> do
              del'' <- checkAssumptions (x, t') sub del' assmps unboxed
              (kind, _, _) <- conv $ synthKind nullSpan g'
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) g' kind) (predicateContext s)
              res <- solve
              if res then
                ctxtMergeFromPure (TyInfix TyOpMeet) [(x, (SVar (Discharged t' g') sInfo depth))] del''
              else none
        _ -> none
  
    -- Additive
    checkAssumptions x add@Additive{} del ((id, SVar (Linear t) sInfo depth):assmps) unboxed =
      case lookupAndCutout id del of
        Just (del', _) ->
          checkAssumptions x add del' assmps unboxed
        _ -> none
    checkAssumptions (x, t') add@Additive{} del ((id, SVar (Discharged t g) sInfo depth):assmps) unboxed = do
          s <- conv get
          case lookupAndCutout id del of
            Just (del', (SVar (Discharged _ g') sInfo' _)) ->
              case lookup id unboxed of
                Just (SVar (Discharged _ g'') sInfo'' _) -> do
                  del'' <- checkAssumptions (x, t') add del' assmps unboxed
                  (kind, _, _) <- conv $ synthKind nullSpan g'
                  -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns g' g'' kind) (predicateContext s)
                  res <- solve
                  if res then
                    ctxtMergeFromPure (TyInfix TyOpJoin) [(x, SVar (Discharged t' g) sInfo depth)] del''
                  else none
                _ -> do
                  del'' <- checkAssumptions (x, t') add del' assmps unboxed
                  (kind, _, _) <- conv $ synthKind nullSpan g
                  -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns g' g kind) (predicateContext s)
                  res <- solve
                  if res then
                    ctxtMergeFromPure (TyInfix TyOpJoin) [(x, SVar (Discharged t' g') sInfo depth)] del''
                  else none
            _ -> do
              (kind, _, _) <- conv $ synthKind nullSpan g
              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) g kind) (predicateContext s)
              res <- solve
              if res then checkAssumptions (x, t') add del assmps unboxed else none
  
    -- Top level definitions should never appear in delta, however, just skip over them if so
    checkAssumptions x mode del (var@(id, SDef{}):assmps) unboxed = checkAssumptions x mode del assmps unboxed
  
  
    -- Construct a typed pattern from an untyped one from the context
    transformPattern ::
         Ctxt (Id, Type)
      -> Type
      -> Ctxt SAssumption
      -> Pattern ()
      -> Ctxt SAssumption
      -> Maybe (Pattern Type, Ctxt (Id, Type))
    transformPattern bindings adt ctxt (PConstr s () b id names pats) unboxed = do
      (pats', bindings') <- transformPatterns bindings adt ctxt pats unboxed
      Just (PConstr s adt b id names pats', bindings)
    transformPattern bindings adt ctxt (PVar s () b name) unboxed =
      let (pat, name', bindings') = case lookup name unboxed of
            Just (SVar (Discharged ty _) _ _) -> (PBox s ty False, name, bindings)
            _ -> (id, name, bindings)
      in
      case lookup name ctxt of
         Just (SVar (Linear t) _ _) -> Just (pat $ PVar s t b name', bindings')
         Just (SVar (Discharged t c) _ _) -> Just (pat $ PVar s t b name', bindings')
         _ -> Nothing
    transformPattern bindings adt ctxt (PBox s () b p) unboxed = do
      (pat', bindings') <- transformPattern bindings adt ctxt p unboxed
      Just (PBox s adt b pat', bindings')
    transformPattern _ _ _ _ _ = Nothing
  
  
    transformPatterns ::
         Ctxt (Id, Type)
      -> Type
      -> Ctxt SAssumption
      -> [Pattern ()]
      -> Ctxt SAssumption
      -> Maybe ([Pattern Type], Ctxt (Id, Type))
    transformPatterns bindings adt ctxt [] unboxed = Just ([], bindings)
    transformPatterns bindings adt ctxt (p:ps) unboxed = do
      (pat, bindings') <- transformPattern bindings adt ctxt p unboxed
      (res, bindingsFinal) <- transformPatterns bindings' adt ctxt ps unboxed
      return (pat:res, bindingsFinal)
  
  constrElimHelper _ _ _ _ _ _ _ _ _ = none
  
  synthesiseInner :: (?globals :: Globals)
             => ResourceScheme PruningScheme
             -> Bool
             -> Depth
             -> FocusPhase
             -> Ctxt SAssumption    -- (unfocused) free variables
             -> FocusedCtxt SAssumption    -- focused variables
             -> Maybe Type
             -> Goal
             -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution, Bindings, Bool)
  synthesiseInner resourceScheme inDef depth focusPhase gamma (Focused omega) grade goal@(Goal goalTySch@(Forall _ _ _ ty) info) = do
  
    currentTime    <- liftIO $ Clock.getTime Clock.Monotonic
  
    -- Synthesiser $ lift $ lift $ lift $ modify (\state ->
              -- state {
                  -- depthReached = if not $ depthReached state then iCurrent depth >= intros depth else True
                    -- })
  
    case (focusPhase, omega) of
      (RightAsync, _) -> do
        varHelper [] (Focused []) (Focused (gamma ++ omega)) resourceScheme grade goal
        `try`
        absHelper gamma (Focused omega) resourceScheme inDef depth RightAsync grade goal
        `try`
        rightAsyncTrans ty
      (LeftAsync, (_:_)) -> do
        varHelper [] (Focused []) (Focused (gamma ++ omega)) resourceScheme grade goal
        `try`
        unboxHelper gamma (Focused []) (Focused omega) resourceScheme inDef depth LeftAsync grade goal
        `try`
        constrElimHelper gamma (Focused []) (Focused omega) resourceScheme inDef depth LeftAsync grade goal
      (LeftAsync, []) -> do
        focus gamma (isRSync ty)
      (RightSync, []) ->
        case not $ isRSync ty of
          True ->
            synthesiseInner resourceScheme inDef depth RightAsync gamma (Focused []) grade goal
          _ ->
            varHelper [] (Focused []) (Focused gamma) resourceScheme grade goal
            `try`
            constrIntroHelper gamma resourceScheme inDef depth RightSync grade goal
            `try`
            boxHelper gamma resourceScheme inDef depth RightSync grade goal
      (LeftSync, var@(x, assumption):[]) -> do
        assumptionTy <- getSAssumptionType assumption
        case assumptionTy of
          (tyA', _, _, _, _, _) ->
            case (not $ isLSync tyA') && (not $ isAtomic tyA') of
              True -> synthesiseInner resourceScheme inDef depth LeftAsync gamma (Focused [var]) grade goal
              _ -> do
                varHelper gamma (Focused []) (Focused omega) resourceScheme grade goal
                `try`
                appHelper gamma (Focused []) (Focused omega) resourceScheme inDef depth LeftSync grade goal
      (LeftSync, []) -> do
          synthesiseInner resourceScheme inDef depth RightAsync gamma (Focused []) grade goal
  
    where
  
      rightAsyncTrans (FunTy{}) = none
      rightAsyncTrans _ = synthesiseInner resourceScheme inDef depth LeftAsync gamma (Focused omega) grade goal
  
      focus gamma True =
        synthesiseInner resourceScheme inDef depth RightSync gamma (Focused []) grade goal
        `try`
        focusLeft [] gamma
      focus gamma False = focusLeft [] gamma
  
      focusLeft _ [] = none
      focusLeft left (var:right) =
        focusLeft (var : left) right
        `try`
        synthesiseInner resourceScheme inDef depth LeftSync (left ++ right) (Focused [var]) grade goal
  
  synthesise :: (?globals :: Globals)
             => ResourceScheme PruningScheme    -- whether the synthesis is in additive mode or not
             -> Ctxt SAssumption    -- (unfocused) free variables
             -> FocusedCtxt SAssumption    -- focused variables
             -> Depth
             -> Maybe Type
             -> Ctxt (Ctxt (TypeScheme, Substitution), Bool)
             -> Goal           -- type from which to synthesise
             -> Synthesiser (Expr () Type, Ctxt SAssumption, Substitution)
  synthesise resourceScheme gamma (Focused omega) depth grade constructorsWithRecs goal = do
  
    st' <- get
    -- relevantConstructors <- do
    --     let snd3 (a, b, c) = b
    --     st <- get
    --     let pats = map (second snd3) (typeConstructors st)
    --     mapM (\ (a, b) -> do
    --         dc <- conv $ mapM (lookupDataConstructor ns) b
    --         let sd = zip (fromJust $ lookup a pats) (catMaybes dc)
    --         return (a, sd)) pats
  
    -- relevantConstructorsWithRecLabels <- mapM (\(tyId, dataCons) -> return (tyId, (dataCons, False))) relevantConstructors -- <- mapM (\(tyId, dataCons) ->
    --                         do
    --                           hasRecCon <- foldM (\a (dataConName, (Forall _ _ _ dataTy)) ->
    --                             case a of
    --                               True -> return True
    --                               _ -> return $ markRecursiveType tyId dataTy
    --                             ) False dataCons
    --                           return (tyId, (dataCons, hasRecCon))) relevantConstructors
  
    Synthesiser $ lift $ lift $ lift $ modify (\state ->
              state {
               constructors = constructorsWithRecs
                    })
  
    result@(expr, ctxt, subst, bindings, _) <- synthesiseInner resourceScheme False depth RightAsync gamma (Focused omega) grade goal
  
    case resourceScheme of
      Subtractive -> do
        -- All linear variables should be gone
        -- and all graded should approximate 0
        consumed <- mapM (\(id, a) ->
                      case a of
                        (SVar Linear{} _ _) -> return False;
                        (SVar (Discharged _ grade) _ _) -> do
                          (kind, _, _) <-  conv $ synthKind nullSpan grade
                          s <- conv get
                          -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) grade kind) (predicateContext s)
                          solve
                        _ -> return True) ctxt
        if and consumed
          then return (expr, ctxt, subst)
          else none
  
      -- All linear variables should have been used
      -- and all graded assumptions should have usages which approximate their original assumption
      Additive{} -> do
        consumed <- mapM (\(id, a) ->
                      case lookup id ctxt of
                        Just (SVar Linear{} _ _) -> return True;
                        Just (SVar (Discharged _ gradeUsed) _ _) ->
                          case a of
                            (SVar (Discharged _ gradeSpec) _ _) -> do
                              (kind, _, _) <- conv $ synthKind nullSpan gradeUsed
                              s <- conv get
                              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns gradeUsed gradeSpec kind) (predicateContext s)
                              solve
                            (SVar (Linear _) _ _) -> return False
                            _ -> return True
                        Just (SDef{}) -> return True
                        Nothing ->
                          case a of
                            (SVar (Discharged _ gradeSpec) _ _) -> do
                              (kind, _, _) <- conv $ synthKind nullSpan gradeSpec
                              s <- conv get
                              -- modifyPred s $ addConstraintViaConjunction (ApproximatedBy ns (TyGrade (Just kind) 0) gradeSpec kind) (predicateContext s)
                              solve
                            (SVar (Linear _) _ _) -> return False
                            _ -> return True) (gamma ++ omega)
        if and consumed
          then return (expr, ctxt, subst)
          else none
  
  
  
  