content: -- Inspired by Adam Gundry et al.'s treatment of type inference in
  -- context. See Gundry's thesis (most closely aligned) or the paper ``Type
  -- inference in Context'' for more details.
  {-# LANGUAGE GADTs #-}
  module TypeCheck where
  
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.Identity
  import Control.Monad.State hiding (modify)
  
  import Data.List.Unique
  
  import qualified Data.Set as S
  import qualified Data.Map.Strict as M
  
  import BwdFwd
  import Syntax
  import FreshNames
  import TypeCheckCommon
  import Unification
  import Debug
  
  import Shonky.Renaming
  
  type EVMap a = M.Map Id (Ab a)
  
  -- Given an operator, reconstruct its corresponding type assigned via context
  -- 1) x is command of interface itf:
  --    - Retrieve how itf is instantiated in amb
  --    - Add mark and add all type variables qs to context (-> qs')
  --    - Unify itf instantiation ps with qs'
  --    - Construct susp. comp. val. type whose containted tys are all in current locality
  -- 2) x is value variable
  --    - It must have been assigned a kind (mono or poly) and a type in the
  --      context. If it is a poly, instantiate the type before returning it.
  find :: Operator Desugared -> Contextual (VType Desugared)
  find (CmdId x a) =
    do amb <- getAmbient
       (itf, qs, rs, ts, y) <- getCmd x
       -- interface itf q_1 ... q_m = x r1 ... r_l: t_1 -> ... -> t_n -> y
       mps <- lkpItf itf 0 amb -- Retrieve how itf is instantiated in amb
       addMark                 -- Localise qs
       -- Make mps flexible if it is not yet and store as res
       res <- case mps of
         Nothing ->
           do b <- isMVarDefined x
              if b then return mps
                else do ps <- mapM (makeFlexibleTyArg []) qs
                        v <- freshMVar "E"
                        let m = ItfMap (M.fromList [(itf, BEmp :< ps)]) a
                        unifyAb amb (Ab (AbFVar v a) m a)
                        return $ Just ps
         Just _ -> return mps
       logBeginFindCmd x itf mps
       case res of
         Nothing -> throwError $ errorFindCmdNotPermit x a itf amb
         Just ps ->
           -- instantiation in ambient: [itf p_1 ... p_m]
           do -- bind qs to their instantiations (according to adjustment) and
              -- localise their occurences in ts, y
              qs' <- mapM (makeFlexibleTyArg []) qs
              ts' <- mapM (makeFlexible []) ts
              y' <- makeFlexible [] y
              zipWithM_ unifyTyArg ps qs'
              -- Localise rs
              rs' <- mapM (makeFlexibleTyArg []) rs
              let ty = SCTy (CType (map (\x -> Port [] x a) ts')
                                   (Peg amb y' a) a) a
              logEndFindCmd x ty
              return ty
  find op@(VarId x _) = getContext >>= find'
    where find' BEmp = throwError $ errorTCNotInScope op
          find' (es :< TermVar (Poly y _) ty) | x == y =
            addMark >> makeFlexible [] ty -- instantiate polymorphic operator
          find' (es :< TermVar (Mono y _) ty) | x == y = return ty
          find' (es :< _) = find' es
  
  -- Find the first flexible type definition (as opposed to a hole) in ctx for x
  findFTVar :: Id -> Contextual (Maybe (VType Desugared))
  findFTVar x = getContext >>= find'
    where find' BEmp = return Nothing
          find' (es :< FlexMVar y (TyDefn ty)) | x == y = return $ Just ty
          find' (es :< _) = find' es
  
  -- Run a contextual computation with an additonal term variable in scope
  -- 1) Push [x:=ty] on context
  -- 2) Run computation m
  -- 3) Remove [x:=ty] from context
  inScope :: Operator Typed -> VType Desugared -> Contextual a -> Contextual a
  inScope x ty m = do modify (:< TermVar x ty)
                      a <- m
                      modify dropVar
                      return a
    where dropVar :: Context -> Context
          dropVar BEmp = error "Invariant violation"
          dropVar (es :< TermVar y _) | strip x == strip y = es
          dropVar (es :< e) = dropVar es :< e
  
  -- Run a contextual computation in a modified ambient environment
  inAmbient :: Ab Desugared -> Contextual a -> Contextual a
  inAmbient amb m = do oldAmb <- getAmbient
                       putAmbient amb
                       a <- m
                       putAmbient oldAmb
                       return a
  
  -- Return the n-th right-most instantiation of the interface in the given
  -- ability. Return Nothing if the interface is not part of the ability.
  lkpItf :: Id -> Int -> Ab Desugared -> Contextual (Maybe [TyArg Desugared])
  lkpItf itf n (Ab v (ItfMap m _) _) =
    case M.lookup itf m of
      Just xs
        | length (bwd2fwd xs) > n -> return $ Just (bwd2fwd xs !! (length (bwd2fwd xs) - n - 1))
        | otherwise               -> lkpItfInAbMod itf (n - length (bwd2fwd xs)) v
      _ -> lkpItfInAbMod itf n v
  
  lkpItfInAbMod :: Id -> Int-> AbMod Desugared -> Contextual (Maybe [TyArg Desugared])
  lkpItfInAbMod itf n (AbFVar x _) = getContext >>= find'
    where find' BEmp = return Nothing
          find' (es :< FlexMVar y (AbDefn ab)) | x == y = lkpItf itf n ab
          find' (es :< _) = find' es
  lkpItfInAbMod itf n v = return Nothing
  
  -- infer the type of a use w.r.t. the given program
  inferEvalUse :: Prog Desugared -> Use Desugared ->
                  Either String (Use Desugared, VType Desugared)
  inferEvalUse p use = runExcept $ evalFreshMT $ evalStateT comp initTCState
    where comp = unCtx $ do _ <- initContextual p
                            inferUse use
  
  -- Main typechecking function
  -- + Init TCState
  -- + Check each top term
  -- + If no exception is thrown during checkTopTm, return input program
  check :: Prog Desugared -> Either String (Prog Desugared)
  check p = runExcept $ evalFreshMT $ evalStateT (checkProg p) initTCState
    where
      checkProg p = unCtx $ do MkProg xs <- initContextual p
                               theCtx <- getContext
                               xs' <- mapM checkTopTm xs
                               return $ MkProg xs'
  
  checkTopTm :: TopTm Desugared -> Contextual (TopTm Desugared)
  checkTopTm (DefTm def a) = DefTm <$> checkMHDef def <*> pure a
  checkTopTm x = return x
  
  checkMHDef :: MHDef Desugared -> Contextual (MHDef Desugared)
  checkMHDef (Def id ty@(CType ps q _) cs a) = do
    ty' <- validateCType ty
    cs' <- mapM (checkCls ty') cs
    return $ Def id ty' cs' a
  
  -- 1st major TC function besides "check": Infer type of a "use"
  -- Functions below implement the typing rules described in the paper.
  -- 1) Var, PolyVar, Command rules
  --    - Find operator x in context and retrieve its (instantiated) type
  --    - Case distinction on x:
  --      1.1) x is monotypic (local var)
  --           - find does no instantiation
  --      1.2) x is polytypic (multi-handler) or a command
  --           - find instantiates any rigid type variables
  -- 2) App rule
  --    - Infer type of f
  --    - If this susp. comp. type is known, check the arguments are well-typed
  --    - If not, create fresh type pattern and unify (constraining for future)
  -- 3) Lift rule
  --    - Get ambient and expand it (substitute all flexible variables)
  --    - Check that instances to be lifted are applicable for this ambient:
  --      - Check "(amb - lifted) + lifted = amb"
  --    - Recursively infer use of term, but under ambient "amb - lifted"
  inferUse :: Use Desugared -> Contextual (Use Desugared, VType Desugared)
  inferUse u@(Op x _) =                                                           -- Var, PolyVar, Command rules
    do logBeginInferUse u
       ty <- find x
       logEndInferUse u ty
       return (u, ty)
  inferUse app@(App f xs a) =                                                     -- App rule
    do logBeginInferUse app
       (f', ty) <- inferUse f
       (xs', res) <- discriminate ty
       logEndInferUse app res
       return (App f' xs' a, res)
    where -- Case distinction on operator's type ty
          -- 1) ty is susp. comp. type
          --    - Check that required abilities of f are admitted (unify with amb)
          --    - Check typings of arguments x_i: p_i in [amb + adj_i] for all i
          -- 2) ty is flex. type var. y
          --    - f must have occured in context as one of these:
          --      2.1) [..., y:=?,   ..., f:=y, ...]
          --           y is not determined yet, create type of right shape
          --           (according to arguments) and constrain ty (unify)
          --      2.2) [..., y:=ty', ..., f:=y, ...]
          --           try 2) again, this time with ty'
          discriminate :: VType Desugared -> Contextual ([Tm Desugared], VType Desugared)
          discriminate ty@(SCTy (CType ps (Peg ab ty' _) _) _) =
          -- {p_1 -> ... p_n -> [ab] ty'}
            do amb <- getAmbient
               -- require ab = amb
               unifyAb ab amb
               -- Check we have the expected number of arguments and the types
               -- match.
               if length xs /= length ps
                 then throwError $ (show $ ppUse f) ++ " expects " ++
                      (show $ length ps) ++ " argument(s) but " ++
                      (show $ length xs) ++ " given " ++
                      "(" ++ (show $ ppSourceOf a) ++ ")"
                 else do xs' <- zipWithM checkArg ps xs
                         return (xs', ty')
          discriminate ty@(FTVar y a) =
            do mty <- findFTVar y  -- find definition of y in context
               case mty of
                 Nothing -> -- 2.1)
                   -- TODO: check that this is correct
                   do addMark
                      amb <- getAmbient
                      ps <- mapM (\_ -> freshPort "X" a) xs
                      q@(Peg ab ty' _)  <- freshPegWithAb amb "Y" a
                      unify ty (SCTy (CType ps q a) a)
                      -- TODO: LC: We have to check typings of x_i for port p_i?
                      -- (didn't appear as a bug yet, but should be examined/fixed eventually)
                      return (xs, ty')
                   -- errTy ty
                 Just ty' -> discriminate ty' -- 2.2)
          discriminate ty = errTy ty
  
          -- TODO: tidy.
          -- We don't need to report an error here, but rather generate
          -- appropriate fresh type variables as above.
          errTy ty = throwError $
                     "application (" ++ show (App f xs (Desugared Generated)) ++
                     "): expected suspended computation but got " ++
                     (show $ ppVType ty)
  
          -- Check typing tm: ty in ambient [adj]
          checkArg :: Port Desugared -> Tm Desugared -> Contextual (Tm Desugared)
          checkArg (Port adjs ty _) tm =
            do amb <- getAmbient >>= expandAb
               (_, amb') <- applyAllAdjustments adjs amb
               inAmbient amb' (checkTm tm ty)
  inferUse adpd@(Adapted adps t a) =
    do logBeginInferUse adpd
       amb <- getAmbient >>= expandAb
       let (Ab v p@(ItfMap m _) _) = amb
       -- Check that the adaptors can be performed and modify the ambient
       -- accordingly
       (adps', amb') <- applyAllAdaptors adps amb
       (t', res) <- inAmbient amb' (inferUse t)
       logEndInferUse adpd res
       return (Adapted adps' t' a, res)
  
  -- 2nd major TC function besides "check": Check that term (construction) has
  -- given type
  checkTm :: Tm Desugared -> VType Desugared -> Contextual (Tm Desugared)
  checkTm (SC sc a) ty = SC <$> (checkSComp sc ty) <*> (pure a)
  checkTm tm@(StrTm _ a) ty = unify (desugaredStrTy a) ty >> return tm
  checkTm tm@(IntTm _ a) ty = unify (IntTy a) ty >> return tm
  checkTm tm@(CharTm _ a) ty = unify (CharTy a) ty >> return tm
  checkTm tm@(TmSeq tm1 tm2 a) ty =
    -- create dummy mvar s.t. any type of tm1 can be unified with it
    do ftvar <- freshMVar "seq"
       tm1' <- checkTm tm1 (FTVar ftvar a)
       tm2' <- checkTm tm2 ty
       return $ TmSeq tm1' tm2' a
  checkTm (Use u a) t = do (u', s) <- inferUse u
                           unify t s
                           return $ Use u' a
  checkTm (DCon (DataCon k xs a') a) ty =
    do (dt, args, ts) <- getCtr k
  --    data dt arg_1 ... arg_m = k t_1 ... t_n | ...
       checkArgs k (length ts) (length xs) a
       addMark
       -- prepare flexible ty vars and ty args
       args' <- mapM (makeFlexibleTyArg []) args
       ts' <- mapM (makeFlexible []) ts
       -- unify with expected type
       unify ty (DTTy dt args' a)
       xs' <- mapM (uncurry checkTm) (zip xs ts')
       return $ DCon (DataCon k xs' a') a
  
  
  -- Check that susp. comp. term has given type, corresponds to Comp rule
  -- Case distinction on expected type:
  -- 1) Check {cls_1 | ... | cls_m} : {p_1 -> ... -> p_n -> q}
  -- 2) Check {cls_1 | ... | cls_m} : ty
  --    - For each cls_i:
  --      - Check against a type of the right shape (of fresh flex. var.s which
  --        then get bound via checking
  --      - Unify the obtained type for cls_i with overall type ty
  checkSComp :: SComp Desugared -> VType Desugared -> Contextual (SComp Desugared)               -- Comp rule
  checkSComp (SComp xs a) (SCTy ty@(CType ps q _) _) = do
    xs' <- mapM (checkCls ty) xs
    return (SComp xs' a)
  checkSComp (SComp xs a) ty = do
    xs' <- mapM (checkCls' ty) xs
    return (SComp xs' a)
    where checkCls' :: VType Desugared -> Clause Desugared ->
                       Contextual (Clause Desugared)
          checkCls' ty cls@(Cls pats tm a) =
            do pushMarkCtx
               ps <- mapM (\_ -> freshPort "X" a) pats
               q <- freshPeg "E" "X" a
               -- {p_1 -> ... -> p_n -> q} for fresh flex. var.s ps, q
               let cty = (CType ps q a)
               cls' <- checkCls cty cls     -- assign these variables
               unify ty (SCTy cty a)        -- unify with resulting ty
               purgeMarks
               return cls'
  
  -- create port <i>X for fresh X
  freshPort :: Id -> Desugared -> Contextual (Port Desugared)
  freshPort x a = do ty <- FTVar <$> freshMVar x <*> pure a
                     return $ Port [] ty a
  
  -- create peg [E|]Y for fresh E, Y
  freshPeg :: Id -> Id -> Desugared -> Contextual (Peg Desugared)
  freshPeg x y a = do v <- AbFVar <$> freshMVar x <*> pure a
                      ty <- FTVar <$> freshMVar y <*> pure a
                      return $ Peg (Ab v (ItfMap M.empty a) a) ty a
  
  -- create peg [ab]X for given [ab], fresh X
  freshPegWithAb :: Ab Desugared -> Id -> Desugared -> Contextual (Peg Desugared)
  freshPegWithAb ab x a = do ty <- FTVar <$> freshMVar x <*> pure a
                             return $ Peg ab ty a
  
  -- Check that given clause has given susp. comp. type (ports, peg)
  checkCls :: CType Desugared -> Clause Desugared ->
              Contextual (Clause Desugared)
  checkCls (CType ports (Peg ab ty _) _) cls@(Cls pats tm a)
  -- type:     port_1 -> ... -> port_n -> [ab]ty
  -- clause:   pat_1     ...    pat_n  =  tm
    | length pats == length ports =
       do pushMarkCtx
          putAmbient ab  -- initialise ambient ability
          bs <- concat <$> zipWithM checkPat pats ports
          -- Bring any bindings in to scope for checking the term then purge the
          -- marks (and suffixes) in the context created for this clause.
          if null bs then -- Just purge marks
                          do tm' <- checkTm tm ty
                             purgeMarks
                             return (Cls pats tm' a)
                     else -- Push all bindings to context, then check tm, then
                          -- remove bindings, finally purge marks.
                          do tm' <- foldl1 (.) (map (uncurry inScope) bs) $ checkTm tm ty
                             purgeMarks
                             return (Cls pats tm' a)
    | otherwise = throwError $ errorTCPatternPortMismatch cls
  
  -- Check that given pattern matches given port
  checkPat :: Pattern Desugared -> Port Desugared -> Contextual [TermBinding]
  checkPat (VPat vp _) (Port _ ty _) = checkVPat vp ty
  checkPat (CmdPat cmd n xs g a) port@(Port adjs ty b) =                                  -- P-Request rule
  -- interface itf q_1 ... q_m =
  --   cmd r_1 ... r_l: t_1 -> ... -> t_n -> y | ...
  
  -- port:     <itf p_1 ... p_m> ty
  -- pattern:  <cmd x_1 ... x_n -> g>
    do (itf, qs, rs, ts, y) <- getCmd cmd
       -- how is itf instantiated in adj?
       let (insts, _) = adjsNormalForm adjs
       let insts' = bwd2fwd $ M.findWithDefault BEmp itf insts
       if length insts' > n then
         do let ps = insts' !! n
            addMark
            -- Flexible ty vars (corresponding to qs)
            skip <- getCmdTyVars cmd
            -- Localise qs, bind them to their instantiation
            -- (according to adjustment) and localise their occurences
            -- in ts, y
            qs' <- mapM (makeFlexibleTyArg skip) qs
            ts' <- mapM (makeFlexible skip) ts
            y' <- makeFlexible skip y
            zipWithM_ unifyTyArg ps qs'
            -- Check command patterns against spec. in interface def.
            bs <- concat <$> mapM (uncurry checkVPat) (zip xs ts')
            -- type of continuation:  {y' -> [adj + currentAmb]ty}
            kty <- contType y' adjs ty a
            -- bindings: continuation + patterns
            return ((Mono g (refToTyped a), kty) : bs)
       else
         throwError $ errorTCCmdNotFoundInPort cmd n port
  checkPat (ThkPat x a) (Port adjs ty b) =                                         -- P-CatchAll rule
  -- pattern:  x
    do amb <- getAmbient
       (_, amb') <- applyAllAdjustments adjs amb
       return [(Mono x (refToTyped a), SCTy (CType [] (Peg amb' ty b) b) b)]
  
  -- continuation type
  contType :: VType Desugared -> [Adjustment Desugared] -> VType Desugared -> Desugared ->
              Contextual (VType Desugared)
  contType x adjs y a =
    do amb <- getAmbient
       (_, amb') <- applyAllAdjustments adjs amb
       return $ SCTy (CType [Port [] x a] (Peg amb' y a) a) a
  
  -- Check that a value pattern has a given type (corresponding to rules)
  -- Return its bindings (id -> value type)
  checkVPat :: ValuePat Desugared -> VType Desugared -> Contextual [TermBinding]
  checkVPat (VarPat x a) ty = return [(Mono x (refToTyped a), ty)]                             -- P-Var rule
  --         x
  checkVPat (DataPat k ps a) ty =                                                 -- P-Data rule
  --         k p_1 .. p_n
    do (dt, args, ts) <- getCtr k
  --   data dt arg_1 .. arg_m = k t_1 .. t_n | ...
       addMark
       args' <- mapM (makeFlexibleTyArg []) args
       ts' <- mapM (makeFlexible []) ts
       unify ty (DTTy dt args' a)
       concat <$> zipWithM checkVPat ps ts'
  checkVPat (CharPat _ a) ty = unify ty (CharTy a) >> return []
  checkVPat (StrPat _ a) ty = unify ty (desugaredStrTy a) >> return []
  checkVPat (IntPat _ a) ty = unify ty (IntTy a) >> return []
  -- checkVPat p ty = throwError $ "failed to match value pattern " ++
  --                  (show p) ++ " with type " ++ (show ty)
  
  
  -- Validate that the adaptors in the ports match the peg. Annotate the
  -- adaptors in the ports accordingly via "applyAllAdjustments".
  validateCType :: CType Desugared -> Contextual (CType Desugared)
  validateCType (CType ps q@(Peg ab ty a') a) = do
    ps' <- mapM validatePort ps
    return $ CType ps' q a
    where
      validatePort :: Port Desugared -> Contextual (Port Desugared)
      validatePort (Port adjs ty a) = do
        (adjs', _) <- applyAllAdjustments adjs ab
        return $ Port adjs' ty a
  
  
  -- Given a list of ids and a type as input, any rigid (val/eff) ty var
  -- contained in ty which does *not* belong to the list is made flexible.
  -- The context is thereby extended.
  -- Case distinction over contained rigid (val/eff) ty var:
  -- 1) it is already part of current locality (up to the Mark)
  --    -> return its occuring name
  -- 2) it is not part of current locality
  --    -> create fresh name in context and return
  makeFlexible :: [Id] -> VType Desugared -> Contextual (VType Desugared)
  makeFlexible skip (DTTy id ts a) = DTTy id <$> mapM (makeFlexibleTyArg skip) ts <*> pure a
  makeFlexible skip (SCTy cty a) = SCTy <$> makeFlexibleCType skip cty <*> pure a
  makeFlexible skip (RTVar x a) | x `notElem` skip = FTVar <$> (getContext >>= find') <*> pure a
  -- find' either creates a new FlexMVar in current locality or identifies the one
  -- already existing
    where find' BEmp = freshMVar x
          find' (es :< FlexMVar y _) | trimVar x == trimVar y = return y
          find' (es :< Mark) = freshMVar x  -- only search in current locality
          find' (es :< _) = find' es
  makeFlexible skip ty = return ty
  
  makeFlexibleAb :: [Id] -> Ab Desugared -> Contextual (Ab Desugared)
  makeFlexibleAb skip (Ab v (ItfMap m _) a) = case v of
    AbRVar x b -> do v' <- if x `notElem` skip then AbFVar <$> (getContext >>= find' x) <*> pure b else return $ AbRVar x b
                     m' <- mapM (mapM (mapM (makeFlexibleTyArg skip))) m
                     return $ Ab v' (ItfMap m' a) a
    _ ->          do m' <- mapM (mapM (mapM (makeFlexibleTyArg skip))) m
                     return $ Ab v (ItfMap m' a) a
  -- find' either creates a new FlexMVar in current locality or identifies the one
  -- already existing
    where find' x BEmp = freshMVar x
          find' x (es :< FlexMVar y _) | trimVar x == trimVar y = return y
          find' x (es :< Mark) = freshMVar x
          find' x (es :< _) = find' x es
  
  makeFlexibleTyArg :: [Id] -> TyArg Desugared -> Contextual (TyArg Desugared)
  makeFlexibleTyArg skip (VArg t a)  = VArg <$> makeFlexible skip t <*> pure a
  makeFlexibleTyArg skip (EArg ab a) = EArg <$> makeFlexibleAb skip ab <*> pure a
  
  makeFlexibleAdj :: [Id] -> Adjustment Desugared -> Contextual (Adjustment Desugared)
  makeFlexibleAdj skip (ConsAdj x ts a) = do ts' <- mapM (makeFlexibleTyArg skip) ts
                                             return $ ConsAdj x ts' a
  makeFlexibleAdj skip (AdaptorAdj adp a) = return $ AdaptorAdj adp a
  
  makeFlexibleCType :: [Id] -> CType Desugared -> Contextual (CType Desugared)
  makeFlexibleCType skip (CType ps q a) = CType <$>
                                           mapM (makeFlexiblePort skip) ps <*>
                                           makeFlexiblePeg skip q <*>
                                           pure a
  
  makeFlexiblePeg :: [Id] -> Peg Desugared -> Contextual (Peg Desugared)
  makeFlexiblePeg skip (Peg ab ty a) = Peg <$>
                                        makeFlexibleAb skip ab <*>
                                        makeFlexible skip ty <*>
                                        pure a
  
  makeFlexiblePort :: [Id] -> Port Desugared -> Contextual (Port Desugared)
  makeFlexiblePort skip (Port adjs ty a) = Port <$>
                                            (mapM (makeFlexibleAdj skip) adjs) <*>
                                            makeFlexible skip ty <*>
                                            pure a
  
  applyAllAdjustments :: [Adjustment Desugared] -> Ab Desugared ->
                         Contextual ([Adjustment Desugared], Ab Desugared)
  applyAllAdjustments [] ab = return ([], ab)
  applyAllAdjustments (adj@(ConsAdj x ts _) : adjr) (Ab v p@(ItfMap m a') a) =
    do let ab' = (Ab v (ItfMap (adjustWithDefault (:< ts) x BEmp m) a') a)
       (adjr', ab'') <- applyAllAdjustments adjr ab'
       return (adj : adjr', ab'')
  applyAllAdjustments ((AdaptorAdj adp a) : adjr) ab =
    do let mAdpAb = applyAdaptor adp ab
       case mAdpAb of
         Just (adp', ab') ->
           do (adjr'', ab'') <- applyAllAdjustments adjr ab'
              return (AdaptorAdj adp' a : adjr'', ab'')
         Nothing -> throwError $ errorAdaptor adp ab
  
  applyAdaptor :: Adaptor Desugared -> Ab Desugared -> Maybe (Adaptor Desugared, Ab Desugared)
  applyAdaptor adp ab@(Ab v p@(ItfMap m a') a) =
    case adpToCompilableAdp ab adp of
      Nothing -> Nothing
      Just adp'@(CompilableAdp x m' ns a'') ->
        let instances = bwd2fwd (M.findWithDefault BEmp x m) in
        -- The indices in ns index from the end of instances, thus we reverse
        -- instances before indexing into it
        let instances' = map (reverse instances !!) ns in
        if null instances' then
          Just (adp', Ab v (ItfMap (M.delete x m) a') a)
        else
          Just (adp', Ab v (ItfMap (
            M.insert x (fwd2bwd instances') m
          ) a') a)
  
  adpToCompilableAdp :: Ab Desugared -> Adaptor Desugared -> Maybe (Adaptor Desugared)
  adpToCompilableAdp (Ab v p@(ItfMap m a') a) adp@(Adp x mm ns a'') =
    let instancesLength = (length . bwd2fwd) (M.findWithDefault BEmp x m) in
    if null ns || instancesLength > maximum ns then
      -- ns is only the xiferp (reverse prefix)
      -- now compute the liat (reverse tail)
      let liat = case mm of
                   Nothing -> []
                   (Just jm) -> reverse [jm .. instancesLength - 1] in
      let ns' = liat ++ ns in
      Just $ CompilableAdp x instancesLength ns' a''
    else Nothing
  adpToCompilableAdp (Ab v p@(ItfMap m a') a) adp@(CompilableAdp x m' ns a'') =
    let instancesLength = (length . bwd2fwd) (M.findWithDefault BEmp x m) in
    if instancesLength == m' then Just adp else Nothing
  
  applyAllAdaptors :: [Adaptor Desugared] -> Ab Desugared -> Contextual ([Adaptor Desugared], Ab Desugared)
  applyAllAdaptors adps ab = do
    -- TODO: LC: kind of not nice, to wrap and then unwrap - implement
    -- differently later?
    let adjs = map (\adp -> AdaptorAdj adp (Desugared Generated)) adps
    (adjs', ab') <- applyAllAdjustments adjs ab
    let adps' = map unwrap adjs'
    return (adps', ab')
    where unwrap :: Adjustment Desugared -> Adaptor Desugared
          unwrap (AdaptorAdj adp _) = adp
          unwrap (ConsAdj _ _ _)    = error "invariant broken"
  
  
  -- helpers
  
  getCtr :: Id -> Contextual (Id,[TyArg Desugared],[VType Desugared])
  getCtr k = get >>= \s -> case M.lookup k (ctrMap s) of
    Nothing -> throwError $ errorTCNotACtr k
    Just (dt, ts, xs) -> return (dt, ts, xs)
  