module Lib.Elab

import Prelude
import Lib.Common
import Lib.Parser.Impl
import Lib.Prettier
import Data.String
import Data.SnocList
import Data.IORef
import Data.SortedMap
import Lib.Eval
import Lib.Util
import Lib.TopContext
-- FIXME Def is shadowing...
import Lib.Syntax
import Lib.Types


vprint : Context -> Val -> M String
vprint ctx v = do
  tm <- quote (length' ctx.env) v
  pure $ render 90 $ pprint (names ctx) tm


-- collectDecl collects multiple Def for one function into one

collectDecl : List Decl -> List Decl
collectDecl Nil = Nil
collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
  if nm == nm' then collectDecl (Def fc nm (cl ++ cl') :: xs)
  else (Def fc nm cl :: collectDecl rest)
collectDecl (x :: xs) = x :: collectDecl xs

rpprint : List String → Tm → String
rpprint names tm = render 90 $ pprint names tm

-- renaming
-- dom gamma ren
data Pden = PR Int Int (List Int)

showCtx : Context -> M String
showCtx ctx =
  unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil
  where
    isVar : Int -> Val -> Bool
    isVar k (VVar _ k' Lin) = k == k'
    isVar _ _ = False

    go : List String -> Int -> List (Val × String × Val) -> List String -> M (List String)
    go _ _ Nil acc = pure acc
    go names k ((v, n, ty) :: xs) acc = if isVar k v
      -- TODO - use Doc and add <+/> as appropriate to printing
      then do
        tty <- quote ctx.lvl ty
        go names (1 + k) xs ("  \{n} : \{rpprint names tty}" :: acc)
      else do
        tm <- quote ctx.lvl v
        tty <- quote ctx.lvl ty
        go names (1 + k) xs ("  \{n} = \{rpprint names tm} : \{rpprint names tty}" :: acc)

dumpCtx : Context -> M String
dumpCtx ctx = do
  let names = (map fst ctx.types)
  -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
  env <- for (zip ctx.env ctx.types) $ \case
    (v, n, ty) => do
      sty <- vprint ctx ty
      sv <- vprint ctx v
      pure "  \{n} : \{sty} = \{sv}"
  let msg = unlines (reverse env) -- ++ "  -----------\n" ++ "  goal \{rpprint names ty'}"
  pure msg



-- return Bnd and type for name

lookupName : Context -> String  -> Maybe (Tm × Val)
lookupName ctx name = go 0 ctx.types
  where
    go : Int -> List (String × Val) -> Maybe (Tm × Val)
    go ix Nil = Nothing
    -- FIXME - we should stuff a Binder of some sort into "types"
    go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (1 + ix) xs


lookupDef : Context -> String  -> Maybe Val
lookupDef ctx name = go 0 ctx.types ctx.env
  where
    go : Int -> List (String × Val) -> List Val -> Maybe Val
    go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs
    go ix _ _ = Nothing


-- IORef for metas needs IO

forceMeta : Val -> M Val
forceMeta (VMeta fc ix sp) = do
  meta <- lookupMeta ix
  case meta of
    (Solved _ k t) => vappSpine t sp >>= forceMeta
    _ => pure (VMeta fc ix sp)
forceMeta x = pure x


record UnifyResult where
  constructor MkResult
  -- wild guess here - lhs is a VVar
  constraints : List (Int × Val)

instance Semigroup UnifyResult where
  (MkResult cs) <+> (MkResult cs') = MkResult (cs ++ cs')

instance Monoid UnifyResult where
  neutral = MkResult Nil

data UnifyMode = UNormal | UPattern



check : Context -> Raw -> Val -> M Tm


unifyCatch : FC -> Context -> Val -> Val -> M Unit

-- Check that the arguments are not explicit and the type constructor in codomain matches
-- Later we will build a table of codomain type, and maybe make the user tag the candidates
-- like Idris does with %hint
isCandidate : Val -> Tm -> Bool
isCandidate ty (Pi fc nm Explicit rig t u) = False
isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u
isCandidate (VRef _ nm _) (Ref fc nm') = nm == nm'
isCandidate ty (App fc t u) = isCandidate ty t
isCandidate _ _ = False

-- This is a crude first pass

findMatches : Context -> Val -> List TopEntry -> M (List String)
findMatches ctx ty Nil = pure Nil
findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
  let (True) = isCandidate ty type | False => findMatches ctx ty xs
  top <- get
  -- let ctx = mkCtx (getFC ty)
  -- FIXME we're restoring state, but the INFO logs have already been emitted
  -- Also redo this whole thing to run during elab, recheck constraints, etc.
  mc <- readIORef top.metaCtx
  catchError (do
      -- TODO sort out the FC here
      let fc = getFC ty
      debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
      -- This check is solving metas, so we save mc below in case we want this solution
      -- tm <- check (mkCtx fc) (RVar fc name) ty
      -- FIXME RVar should optionally have qualified names
      let (QN ns nm) = name

      let (cod, tele) = splitTele type
      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
      tm <- check ctx (RVar fc nm) ty
      debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
      writeIORef top.metaCtx mc
      (_::_ nm) <$> findMatches ctx ty xs)
    (\ err => do
      debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}"
      writeIORef top.metaCtx mc
      findMatches ctx ty xs)


contextMatches : Context -> Val -> M (List (Tm × Val))
contextMatches ctx ty = go (zip ctx.env ctx.types)
  where
    go : List (Val × String × Val) -> M (List (Tm × Val))
    go Nil = pure Nil
    go ((tm, nm, vty) :: xs) = do
      type <- quote ctx.lvl vty
      let (True) = isCandidate ty type | False => go xs
      top <- get
      mc <- readIORef top.metaCtx
      catchError(do
          debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}"
          unifyCatch (getFC ty) ctx ty vty
          mc' <- readIORef top.metaCtx
          writeIORef top.metaCtx mc
          tm <- quote ctx.lvl tm
          (_::_ (tm, vty)) <$> go xs)
        (\ err => do
          debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}"
          writeIORef top.metaCtx mc
          go xs)


getArity : Tm -> Int
getArity (Pi x str icit rig t u) = 1 + getArity u
-- Ref or App (of type constructor) are valid
getArity _ = 0

-- Can metas live in context for now?
-- We'll have to be able to add them, which might put gamma in a ref



-- Makes the arg for `solve` when we solve an auto
makeSpine : Int -> List BD -> SnocList Val
makeSpine k Nil = Lin
makeSpine k (Defined :: xs) = makeSpine (k - 1) xs
makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin


solve : Env -> QName -> SnocList Val -> Val -> M Unit



trySolveAuto : MetaEntry -> M Bool
trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
      debug $ \ _ => "TRYAUTO solving \{show k} : \{show ty}"
      -- fill in solved metas in type
      x <- quote ctx.lvl ty
      ty <- eval ctx.env CBN x
      debug $ \ _ => "AUTO ---> \{show ty}"
      -- we want the context here too.
      top <- get
      Nil <- contextMatches ctx ty
          | ((tm, vty) :: Nil) => do
              unifyCatch (getFC ty) ctx ty vty
              val <- eval ctx.env CBN tm
              debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
              let sp = makeSpine ctx.lvl ctx.bds
              solve ctx.env k sp val
              pure True
          | res => do
              debug $ \ _ => "FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
              pure False
      let te = listValues top.defs
      let rest = map {List} (\ x => listValues x.modDefs) $
            mapMaybe (flip lookupMap' top.modules) top.imported

      (nm :: Nil) <- findMatches ctx ty $ join (te :: rest)
        | res => do
          debug $ \ _ => "FAILED to solve \{show ty}, matches: \{show res}"
          pure False
      tm <- check ctx (RVar fc nm) ty
      val <- eval ctx.env CBN tm
      debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
      let sp = makeSpine ctx.lvl ctx.bds
      solve ctx.env k sp val
      pure True
trySolveAuto _ = pure False

-- export
-- solveAutos : Int -> List MetaEntry -> M Unit
-- solveAutos mstart Nil = pure MkUnit
-- solveAutos mstart (entry :: es) = do
--       res <- trySolveAuto entry
--       -- idris is inlining this and blowing stack?
--       if res
--         then do
--           top <- get
--           mc <- readIORef top.metaCtx
--           let mlen = length mc.metas `minus` mstart
--           solveAutos mstart (take mlen mc.metas)
--         else
--           solveAutos mstart es


-- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't
-- handle the traversal of the entire meta list.  I've turned the restart into a trampoline
-- and filtered it down to unsolved autos.

solveAutos : Int -> M Unit
solveAutos mstart = do
  top <- get
  mc <- readIORef top.metaCtx

  res <- run $ filter isAuto (listValues mc.metas)
  if res then solveAutos mstart else pure MkUnit
  where
    isAuto : MetaEntry -> Bool
    isAuto (Unsolved fc k ctx x AutoSolve xs) = True
    isAuto _ = False

    run : List MetaEntry -> M Bool
    run Nil = pure False
    run (e :: es) = do
      res <- trySolveAuto e
      if res then pure True else run es

-- We need to switch to SortedMap here

updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit
updateMeta ix f = do
  top <- get
  mc <- readIORef {M} top.metaCtx
  let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit
  me <- f me
  writeIORef top.metaCtx $ MC (updateMap ix me mc.metas) mc.next mc.mcmode


checkAutos : QName -> List MetaEntry -> M Unit
checkAutos ix Nil = pure MkUnit
checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do
  ty' <- quote ctx.lvl ty
  when (usesMeta ty') $ \ _ => ignore $ trySolveAuto entry
  checkAutos ix rest
  where
    usesMeta : Tm -> Bool
    usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u
    usesMeta (App _ _ u) = usesMeta u
    usesMeta _ = False
checkAutos ix (_ :: rest) = checkAutos ix rest


addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
addConstraint env ix sp tm = do
  top <- get
  mc <- readIORef top.metaCtx
  let (CheckAll) = mc.mcmode | _ => pure MkUnit
  updateMeta ix $ \case
    (Unsolved pos k a b c cons) => do
      debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
      pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
    (Solved _ k tm) => error' "Meta \{show k} already solved [addConstraint]"
    (OutOfScope) => error' "Meta \{show ix} out of scope"
  mc <- readIORef top.metaCtx
  checkAutos ix (listValues mc.metas)
  -- this loops too
  -- solveAutos 0 mc.metas
  pure MkUnit


-- return renaming, the position is the new VVar
invert : Int -> SnocList Val -> M (List Int)
invert lvl sp = go sp Nil
  where
    go : SnocList Val -> List Int -> M (List Int)
    go Lin acc = pure $ reverse acc
    go (xs :< VVar fc k Lin) acc = do
      if elem k acc
        then do
          debug $ \ _ => "\{show k} \{show acc}"
          -- when does this happen?
          error fc "non-linear pattern: \{show sp}"
        else go xs (k :: acc)
    go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}"


-- REVIEW why am I converting to Tm?
-- we have to "lift" the renaming when we go under a lambda
-- I think that essentially means our domain ix are one bigger, since we're looking at lvl
-- in the codomain, so maybe we can just keep that value

rename : QName -> List Int -> Int -> Val  -> M Tm

renameSpine : QName -> List Int -> Int -> Tm -> SnocList Val  -> M Tm
renameSpine meta ren lvl tm Lin = pure tm
renameSpine meta ren lvl tm (xs :< x) = do
  xtm <- rename meta ren lvl x
  xs' <- renameSpine meta ren lvl tm xs
  pure $ App emptyFC xs' xtm

rename meta ren lvl (VVar fc k sp) = case findIndex' (_==_ k) ren of
  Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}"
  Just x => renameSpine meta ren lvl (Bnd fc x) sp
rename meta ren lvl (VRef fc nm sp) = renameSpine meta ren lvl (Ref fc nm) sp
rename meta ren lvl (VMeta fc ix sp) = do
  -- So sometimes we have an unsolved meta in here which reference vars out of scope.
  debug $ \ _ => "rename Meta \{show ix} spine \{show sp}"
  if ix == meta
  -- REVIEW is this the right fc?
    then error fc "meta occurs check"
    else do
      meta' <- lookupMeta ix
      case meta' of
        Solved fc _ val => do
          debug $ \ _ => "rename: \{show ix} is solved"
          val' <- vappSpine val sp
          rename meta ren lvl val'
        _ => do
          debug $ \ _ => "rename: \{show ix} is unsolved"
          catchError (renameSpine meta ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err))
rename meta ren lvl (VLam fc n icit rig t) = do
  tapp <- t $$ VVar fc lvl Lin
  scope <- rename meta (lvl :: ren) (1 + lvl) tapp
  pure (Lam fc n icit rig scope)
rename meta ren lvl (VPi fc n icit rig ty tm) = do
  ty' <- rename meta ren lvl ty
  tmapp <- tm $$ VVar emptyFC lvl Lin
  scope' <- rename meta (lvl :: ren) (1 + lvl) tmapp
  pure (Pi fc n icit rig ty' scope')
rename meta ren lvl (VU fc) = pure (UU fc)
rename meta ren lvl (VErased fc) = pure (Erased fc)
-- for now, we don't do solutions with case in them.
rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution"
rename meta ren lvl (VLit fc lit) = pure (Lit fc lit)
rename meta ren lvl (VLet fc name val body) = do
  val' <- rename meta ren lvl val
  body' <- rename meta (lvl :: ren) (1 + lvl) body
  pure $ Let fc name val' body'
-- these probably shouldn't show up in solutions...
rename meta ren lvl (VLetRec fc name ty val body) = do
  ty' <- rename meta ren lvl ty
  val' <- rename meta (lvl :: ren) (1 + lvl) val
  body' <- rename meta (lvl :: ren) (1 + lvl) body
  pure $ LetRec fc name ty' val' body'

lams : Nat -> List String -> Tm -> Tm
lams Z _ tm = tm
-- REVIEW do we want a better FC, icity?, rig?
lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm)
lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm)


unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult

.boundNames : Context -> List String
ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ zip ctx.bds (map fst ctx.types)

maybeCheck : M Unit -> M Unit
maybeCheck action = do
  top <- get
  mc <- readIORef top.metaCtx
  case mc.mcmode of
    CheckAll => action
    CheckFirst => do
      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next NoCheck
      action
      modifyIORef top.metaCtx $ \ mc => MC mc.metas mc.next CheckFirst
    NoCheck => pure MkUnit

solve env m sp t = do
  meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
    | _ => error (getFC t) "Meta \{show m} already solved! [solve]"
  debug $ \ _ => "SOLVE \{show m} \{show kind} lvl \{show $ length' env} sp \{show sp} is \{show t}"
  let size = length $ filter (\x => x == Bound) ctx_.bds
  debug $ \ _ => "\{show m} size is \{show size} sps \{show $ snoclen sp}"
  let (True) = snoclen sp == size
    | _ => do
      let l = length' env
      debug $ \ _ => "meta \{show m} (\{show ix}) applied to \{show $ snoclen sp} args instead of \{show size}"
      debug $ \ _ => "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}"
      addConstraint env m sp t
  let l = length' env
  debug $ \ _ => "meta \{show meta}"
  ren <- invert l sp
  -- force unlet
  hack <- quote l t
  t <- eval env CBN hack
  catchError (do
    tm <- rename m ren l t

    let tm = lams (snoclen sp) (reverse ctx_.boundNames) tm
    top <- get
    soln <- eval Nil CBN tm

    updateMeta m $ \case
      (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
      (Solved _ k x) => error' "Meta \{show ix} already solved! [solve2]"
      OutOfScope => error' "Meta \{show ix} out of scope"
    maybeCheck $ for_ cons $ \case
      MkMc fc env sp rhs => do
        val <- vappSpine soln sp
        debug $ \ _ => "discharge l=\{show $ length' env} \{(show val)} =?= \{(show rhs)}"
        unify env UNormal val rhs
    mc <- readIORef top.metaCtx
    -- stack ...
    -- checkAutos ix mc.metas
    pure MkUnit
    )

    (\case
      Postpone fc ix msg => do
        -- let someone else solve this and then check again.
        debug $ \ _ => "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}"
        addConstraint env m sp t
        -- I get legit errors after stuffing in solution
        -- report for now, tests aren't hitting this branch
      err => throwError err
        -- debug $ \ _ => "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}"
        -- debug $ \ _ => "because \{showError "" err}"
        -- addConstraint env m sp t
        )

unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now
unifySpine env mode True Lin Lin = pure (MkResult Nil)
unifySpine env mode True (xs :< x) (ys :< y) =
  -- I had idiom brackets here, technically fairly easy to desugar, but not adding at this time
  _<+>_ <$> unify env mode x y <*> unifySpine env mode True xs ys
unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch"


unify env mode t u = do
  debug $ \ _ => "Unify lvl \{show $ length env}"
  debug $ \ _ => "  \{show t}"
  debug $ \ _ => "  =?= \{show u}"
  t' <- forceMeta t >>= unlet env
  u' <- forceMeta u >>= unlet env
  debug $ \ _ => "forced \{show t'}"
  debug $ \ _ => "  =?= \{show u'}"
  debug $ \ _ => "env \{show env}"
  -- debug $ \ _ => "types \{show $ ctx.types}"
  let l = length' env
  -- On the LHS, variable matching is yields constraints/substitutions
  -- We want this to happen before VRefs are expanded, and mixing mode
  -- into the case tree explodes it further.
  case mode of
    UPattern => unifyPattern t' u'
    UNormal => unifyMeta t' u'

  -- The case tree is still big here. It's hard for idris to sort
  -- What we really want is what I wrote - handle meta, handle lam, handle var, etc

  where
    -- The case tree here was huge, so I split it into stages
    -- newt will have similar issues because it doesn't emit a default case

    unifyRest : Val -> Val -> M UnifyResult
    unifyRest (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do
      let fresh = VVar fc (length' env) Lin
      xb <- b $$ fresh
      xb' <- b' $$ fresh
      _<+>_ <$> unify env mode a a' <*> unify (fresh :: env) mode xb xb'

    unifyRest (VU _) (VU _) = pure neutral
    -- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
    unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n  env is \{show env}"

    unifyRef : Val -> Val -> M UnifyResult
    unifyRef t'@(VRef fc k sp)  u'@(VRef fc' k' sp') =
      -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y
        do
        -- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do
            Nothing <- tryEval env t'
              | Just v => do
                  debug $ \ _ => "tryEval \{show t'} to \{show v}"
                  unify env mode v u'
            Nothing <- tryEval env u'
              | Just v => unify env mode t' v
            if k == k'
              then unifySpine env mode (k == k') sp sp'
              else error fc "vref mismatch \{show t'} \{show u'}"

    -- Lennart.newt cursed type references itself
    -- We _could_ look up the ref, eval against Nil and vappSpine...
    unifyRef t         u@(VRef fc' k' sp') = do
      debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
      top <- get
      case lookup k' top of
        Just (MkEntry _ name ty (Fn tm)) => do
          vtm <- eval Nil CBN tm
          appvtm <- vappSpine vtm sp'
          unify env mode t appvtm
        _ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n  env is \{show env}"

    unifyRef t@(VRef fc k sp) u = do
      debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
      top <- get
      case lookup k top of
        Just (MkEntry _ name ty (Fn tm)) => do
          vtm <- eval Nil CBN tm
          tmsp <- vappSpine vtm sp
          unify env mode tmsp u
        _ => error fc "unify failed \{show t} (no Fn :: Nil) =?= \{show u}\n  env is \{show env}"
    unifyRef t u = unifyRest t u

    unifyVar : Val -> Val -> M UnifyResult
    unifyVar t'@(VVar fc k sp)  u'@(VVar fc' k' sp')  =
      if k == k' then unifySpine env mode (k == k') sp sp'
      else error fc "Failed to unify \{show t'} and \{show u'}"

    unifyVar t'@(VVar fc k Lin) u = do
      vu <- tryEval env u
      case vu of
        Just v => unify env mode t' v
        Nothing => error fc "Failed to unify \{show t'} and \{show u}"

    unifyVar t u'@(VVar fc k Lin) = do
      vt <- tryEval env t
      case vt of
        Just v => unify env mode v u'
        Nothing => error fc "Failed to unify \{show t} and \{show u'}"
    unifyVar t u = unifyRef t u

    unifyLam : Val -> Val -> M UnifyResult
    unifyLam (VLam fc _ _ _ t)  (VLam _ _ _ _ t') = do
      let fresh = VVar fc (length' env) Lin
      vappt <- t $$ fresh
      vappt' <- t' $$ fresh
      unify (fresh :: env) mode vappt vappt'
    unifyLam t         (VLam fc' _ _ _ t') = do
      debug $ \ _ => "ETA \{show t}"
      let fresh = VVar fc' (length' env) Lin
      vappt <- vapp t fresh
      vappt' <- t' $$ fresh
      unify (fresh :: env) mode vappt vappt'
    unifyLam (VLam fc _ _ _ t)  t'     = do
      debug $ \ _ => "ETA' \{show t'}"
      let fresh = VVar fc (length' env) Lin
      appt <- t $$ fresh
      vappt' <- vapp t' fresh
      unify (fresh :: env) mode appt vappt'
    unifyLam t u = unifyVar t u

    unifyMeta : Val -> Val -> M UnifyResult
    -- flex/flex
    unifyMeta (VMeta fc k sp) (VMeta fc' k' sp') =
      if k == k' then unifySpine env mode (k == k') sp sp'
      -- TODO, might want to try the other way, too.
      else if snoclen sp < snoclen sp'
        then solve env k' sp' (VMeta fc k sp) >> pure neutral
        else solve env k sp (VMeta fc' k' sp') >> pure neutral
    unifyMeta t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral
    unifyMeta (VMeta fc i sp) t' = solve env i sp t' >> pure neutral
    unifyMeta t v = unifyLam t v

    unifyPattern : Val -> Val -> M UnifyResult
    unifyPattern t'@(VVar fc k sp)  u'@(VVar fc' k' sp')  =
      if k == k' then unifySpine env mode (k == k') sp sp'
      else case (sp, sp') of
        (Lin,Lin) => if k < k'
          then pure $ MkResult ((k, u') :: Nil)
          else pure $ MkResult ((k', t') :: Nil)
        _ => error fc "Failed to unify \{show t'} and \{show u'}"

    unifyPattern (VVar fc k Lin) u = pure $ MkResult((k, u) :: Nil)
    unifyPattern t (VVar fc k Lin) = pure $ MkResult ((k, t) :: Nil)
    unifyPattern t u = unifyMeta t u


unifyCatch fc ctx ty' ty = do
    res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do
      let names = map fst ctx.types
      debug $ \ _ => "fail \{show ty'} \{show ty}"
      a <- quote ctx.lvl ty'
      b <- quote ctx.lvl ty
      let msg = "unification failure: \{errorMsg err}\n  failed to unify \{rpprint names a}\n             with \{rpprint names b}\n  "
      throwError (E fc msg)
    case res of
      MkResult Nil => pure MkUnit
      cs => do
        -- probably want a unification mode that throws instead of returning constraints
        -- TODO need a normalizeHoles, maybe on quote?
        debug $ \ _ => "fail with constraints \{show cs.constraints}"
        a <- quote ctx.lvl ty'
        b <- quote ctx.lvl ty
        let names = map fst ctx.types
        let msg = "unification failure\n  failed to unify \{rpprint names a}\n             with \{rpprint names b}"
        let msg = msg ++ "\nconstraints \{show cs.constraints}"
        throwError (E fc msg)
        -- error fc "Unification yields constraints \{show cs.constraints}"


freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
freshMeta ctx fc ty kind = do
  top <- get
  mc <- readIORef top.metaCtx
  debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
  -- need the ns here
  -- we were fudging this for v1
  let qn = QN top.ns "$m\{show mc.next}"
  let newmeta = Unsolved fc qn ctx ty kind Nil
  writeIORef top.metaCtx $ MC (updateMap qn newmeta mc.metas) (1 + mc.next) mc.mcmode
  -- infinite loop - keeps trying Ord a => Ord (a \x a)
  -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta
  pure $ applyBDs 0 (Meta fc qn) ctx.bds
  where
    -- hope I got the right order here :)
    applyBDs : Int -> Tm -> List BD -> Tm
    applyBDs k t Nil = t
    -- review the order here
    applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k)
    applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs

insert : (ctx : Context) -> Tm -> Val -> M (Tm × Val)
insert ctx tm ty = do
  ty' <- forceMeta ty
  case ty' of
    VPi fc x Auto rig a b => do
      m <- freshMeta ctx (getFC tm) a AutoSolve
      debug $ \ _ => "INSERT Auto \{rpprint (names ctx) m} : \{show a}"
      debug $ \ _ => "TM \{rpprint (names ctx) tm}"
      mv <- eval ctx.env CBN m
      bapp <- b $$ mv
      insert ctx (App (getFC tm) tm m) bapp
    VPi fc x Implicit rig a b => do
      m <- freshMeta ctx (getFC tm) a Normal
      debug $ \ _ => "INSERT \{rpprint (names ctx) m} : \{show a}"
      debug $ \ _ => "TM \{rpprint (names ctx) tm}"
      mv <- eval ctx.env CBN m
      bapp <- b $$ mv
      insert ctx (App (getFC tm) tm m) bapp
    va => pure (tm, va)

primType : FC -> QName -> M Val
primType fc nm = do
  top <- get
  case lookup nm top of
      Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name Lin
      _ => error fc "Primitive type \{show nm} not in scope"


infer : Context -> Raw  -> M (Tm × Val)


data Bind = MkBind String Icit Val

instance Show Bind where
  show (MkBind str icit x) = "\{str} \{show icit}"


---------------- Case builder


record Problem where
  constructor MkProb
  clauses : List Clause
  -- I think a pi-type representing the pattern args -> goal, so we're checking
  -- We might pull out the pattern abstraction to a separate step and drop pats from clauses.
  ty : Val

-- Might have to move this if Check reaches back in...
-- this is kinda sketchy, we can't use it twice at the same depth with the same name.
fresh : {{ctx : Context}} -> String -> String
fresh {{ctx}} base = base ++ "$" ++ show (length' ctx.env)

-- The result is a casetree, but it's in Tm

buildTree : Context -> Problem -> M Tm

-- Updates a clause for INTRO
introClause : String -> Icit -> Clause -> M Clause
introClause nm icit (MkClause fc cons (pat :: pats) expr) =
  if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr
  else if icit == Implicit then pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) (pat :: pats) expr
  else if icit == Auto then pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) (pat :: pats) expr
  else error fc "Explicit arg and \{show $ getIcit pat} pattern \{show nm}  \{show pat}"
-- handle implicts at end?
introClause nm Implicit (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) Nil expr
introClause nm Auto (MkClause fc cons Nil expr) = pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) Nil expr
introClause nm icit (MkClause fc cons Nil expr) = error fc "Clause size doesn't match"

-- A split candidate looks like x /? Con ...
-- we need a type here. I pulled if off of the
-- pi-type, but do we need metas solved or dependents split?
-- this may dot into a dependent.
findSplit : List Constraint -> Maybe Constraint
findSplit Nil = Nothing
    -- FIXME look up type, ensure it's a constructor
findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x
findSplit (x@(nm, PatLit _ val) :: xs) = Just x
findSplit (x :: xs) = findSplit xs


-- ***************
-- right, I think we rewrite the names in the context before running raw and we're good to go?
-- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was?

-- we could pass into build case and use it for   (x /? y)

-- TODO, we may need to filter these against the type to rule out
-- impossible cases
getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm))
getConstructors ctx scfc (VRef fc nm _) = do
  names <- lookupTCon nm
  traverse lookupDCon names
  where
    lookupTCon : QName -> M (List QName)
    lookupTCon str = do
      top <- get
      case lookup nm top of
        (Just (MkEntry _ name type (TCon names))) => pure names
        _ => error scfc "Not a type constructor \{show nm}"
    lookupDCon : QName -> M (QName × Int × Tm)
    lookupDCon nm = do
      top <- get
      case lookup nm top of
        (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type)
        Just _ => error fc "Internal Error: \{show nm} is not a DCon"
        Nothing => error fc "Internal Error: DCon \{show nm} not found"
getConstructors ctx scfc tm = do
  tms <- vprint ctx tm
  error scfc "Can't split - not VRef: \{tms}"

-- Extend environment with fresh variables from a pi-type
-- the pi-type here is the telescope of a constructor
-- return context, remaining type, and list of names
extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context × Val × List Bind × SnocList Val)
extendPi ctx (VPi x str icit rig a b) nms sc = do
    let nm = fresh str -- "pat"
    let ctx' = extend ctx nm a
    let v = VVar emptyFC (length' ctx.env) Lin
    tyb <- b $$ v
    extendPi ctx' tyb (nms :< MkBind nm icit a) (sc :< VVar x (length' ctx.env) Lin)
extendPi ctx ty nms sc = pure (ctx, ty, nms <>> Nil, sc)

-- turn vars into lets for forced values.
-- substitute inside values
-- FIXME we're not going under closures at the moment.
substVal : Int -> Val -> Val -> Val
substVal k v tm = go tm
  where
    go : Val -> Val
    go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp))
    go (VLet fc nm a b) = VLet fc nm (go a) b
    go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b
    go (VMeta fc ix sp) = VMeta fc ix (map go sp)
    go (VRef fc nm sp) = VRef fc nm (map go sp)
    go tm = tm
    -- FIXME - do I need a Val closure like idris?
    -- or env in unify...
    -- or quote back
    -- go (VLam fc nm sc) = VLam fc nm sc
    -- go (VCase x sc xs) = ?rhs_2
    -- go (VU x) = ?rhs_7
    -- go (VLit x y) = ?rhs_8


-- need to turn k into a ground value

-- TODO rework this to do something better.  We've got constraints, and
-- and may need to do proper unification if it's already defined to a value
-- below we're handling the case if it's defined to another var, but not
-- checking for loops.
updateContext : Context -> List (Int × Val) -> M Context
updateContext ctx Nil = pure ctx
updateContext ctx ((k, val) :: cs) =
  let ix = cast $ lvl2ix (length' ctx.env) k in
  case getAt ix ctx.env of
    (Just (VVar _ k' Lin)) =>
      if k' /= k
        then updateContext ctx ((k',val) :: cs)
        else
          let ctx' = MkCtx ctx.lvl (map (substVal k val) ctx.env) ctx.types (replaceV ix Defined ctx.bds) ctx.ctxFC
          in updateContext ctx' cs
    (Just val') => do
      -- This is fine for Z =?= Z but for other stuff, we probably have to match
      info (getFC val) "need to unify \{show val} and \{show val'} or something"
      updateContext ctx cs
    Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext"

  --
  -- updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs
  where
    replace : Nat -> Val -> List Val -> List Val
    replace k x Nil = Nil
    replace Z x (y :: xs) = x :: xs
    replace (S k) x (y :: xs) = y :: replace k x xs

    replaceV : ∀ a. Nat -> a -> List a -> List a
    replaceV k x Nil = Nil
    replaceV Z x (y :: xs) = x :: xs
    replaceV (S k) x (y :: xs) = y :: replaceV k x xs

checkCase : Context → Problem → String → Val → (QName × Int × Tm) → M Bool
checkCase ctx prob scnm scty (dcName, arity, ty) = do
  vty <- eval Nil CBN ty
  (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin
  (Just res) <- catchError (Just <$> unify ctx'.env UPattern ty' scty)
              (\err => do
                  debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
                  pure Nothing)
    | _ => pure False

  (Right res) <- tryError (unify ctx'.env UPattern ty' scty)
          | Left err => do
            debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
            pure False

  case lookupDef ctx scnm of
    Just val@(VRef fc nm sp) => pure $ nm == dcName
    _ => pure True

-- ok, so this is a single constructor, CaseAlt
-- return Nothing if dcon doesn't unify with scrut
buildCase : Context -> Problem -> String -> Val -> (QName × Int × Tm) -> M (Maybe CaseAlt)
buildCase ctx prob scnm scty (dcName, arity, ty) = do
  debug $ \ _ => "CASE \{scnm} match \{show dcName} ty \{rpprint (names ctx) ty}"
  vty <- eval Nil CBN ty
  (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin

  -- TODO I think we need to figure out what is dotted, maybe
  -- the environment manipulation below is sufficient bookkeeping
  -- or maybe it's a bad approach.

  -- At some point, I'll take a break and review more papers and code,
  -- now that I know some of the questions I'm trying to answer.

  -- We get unification constraints from matching the data constructors
  -- codomain with the scrutinee type
  debug $ \ _ => "unify dcon cod with scrut\n  \{show ty'}\n  \{show scty}"
  Just res <- catchError(Just <$> unify ctx'.env UPattern ty' scty)
              (\err => do
                  debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
                  pure Nothing)
    | _ => pure Nothing

  -- if the value is already constrained to a different constructor, return Nothing
  debug $ \ _ => "scrut \{scnm} constrained to \{show $ lookupDef ctx scnm}"
  let (VRef _ sctynm _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}"

  case lookupDef ctx scnm of
    Just val@(VRef fc nm sp) =>
      if nm /= dcName
      then do
        debug $ \ _ => "SKIP \{show dcName} because \{scnm} forced to \{show val}"
        pure Nothing
      else do
        debug $ \ _ => "case \{show dcName} dotted \{show val}"
        when (length vars /= snoclen sp) $ \ _ => error emptyFC "\{show $ length vars} vars /= \{show $ snoclen sp}"

        -- TODO - I think we need to define the context vars to sp via updateContext

        let lvl = length' ctx'.env - length' vars
        let scons = constrainSpine lvl (sp <>> Nil) -- REVIEW is this the right order?
        ctx' <- updateContext ctx' scons

        debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
        debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were"
        for prob.clauses $ (\x => debug $ \ _ => "    \{show x}")
        clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
        debug $ \ _ => "and now:"
        for clauses $ (\x => debug $ \ _ => "    \{show x}")
        when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}"
        tm <- buildTree ctx' (MkProb clauses prob.ty)
        pure $ Just $ CaseCons dcName (map getName vars) tm

    _ => do
        (Right res) <- tryError (unify ctx'.env UPattern ty' scty)
          | Left err => do
            debug $ \ _ => "SKIP \{show dcName} because unify error \{errorMsg err}"
            pure Nothing

        -- Constrain the scrutinee's variable to be dcon applied to args
        let (Just x) = findIndex' ((_==_ scnm) ∘ fst) ctx'.types
          | Nothing => error ctx.ctxFC "\{scnm} not is scope?"
        let lvl = lvl2ix (length' ctx'.env) x
        let scon = (lvl, VRef ctx.ctxFC dcName sc) -- (DCon arity dcName)

        debug $ \ _ => "scty \{show scty}"
        debug $ \ _ => "UNIFY results \{show res.constraints}"
        debug $ \ _ => "before types: \{show ctx'.types}"
        debug $ \ _ => "before env: \{show ctx'.env}"
        debug $ \ _ => "SC CONSTRAINT: \{show scon}"

        -- push the constraints into the environment by turning bind into define
        -- Is this kosher?  It might be a problem if we've already got metas over
        -- this stuff, because it intends to ignore defines.
        ctx' <- updateContext ctx' (scon :: res.constraints)

        debug $ \ _ => "context types: \{show ctx'.types}"
        debug $ \ _ => "context env: \{show ctx'.env}"

        -- What if all of the pattern vars are defined to meta

        debug $ \ _ => "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
        debug $ \ _ => "(dcon \{show dcName}) (vars \{show vars}) clauses were"
        for prob.clauses $ (\x => debug $ \ _ => "    \{show x}")
        clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
        debug $ \ _ => "and now:"
        for clauses $ (\x => debug $ \ _ => "    \{show x}")
        when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show dcName} splitting \{scnm}"
        tm <- buildTree ctx' (MkProb clauses prob.ty)
        pure $ Just $ CaseCons dcName (map getName vars) tm
  where
    constrainSpine : Int -> List Val -> List (Int × Val)
    constrainSpine lvl Nil = Nil
    constrainSpine lvl (v :: vs) = (lvl, v) :: constrainSpine (1 + lvl) vs

    getName : Bind -> String
    getName (MkBind nm _ _) = nm

    -- for each clause in prob, find nm on LHS of some constraint, and
    -- "replace" with the constructor and vars.
    --
    -- This will be:
    --   x /? y    can probably just leave this
    --   x /? D a b c  split into three x /? a, y /? b, z /? c
    --   x /? E a b    drop this clause
    -- We get a list of clauses back (a Problem) and then solve that
    -- If they all fail, we have a coverage issue. (Assuming the constructor is valid)

    makeConstr : FC -> List Bind -> List Pattern -> M (List (String × Pattern))
    makeConstr fc Nil Nil = pure $ Nil
    makeConstr fc Nil (pat :: pats) = error (getFC pat) "too many patterns"
    makeConstr fc ((MkBind nm Implicit x) :: xs) Nil = do
      rest <- makeConstr fc xs Nil
      pure $ (nm, PatWild emptyFC Implicit) :: rest
    makeConstr fc ((MkBind nm Auto x) :: xs) Nil = do
      rest <- makeConstr fc xs Nil
      pure $ (nm, PatWild emptyFC Auto) :: rest
    makeConstr fc ((MkBind nm Explicit x) :: xs) Nil = error fc "not enough patterns"
    makeConstr fc ((MkBind nm Explicit x) :: xs) (pat :: pats) =
      if getIcit pat == Explicit
        then do
          rest <- makeConstr fc xs pats
          pure $ (nm, pat) :: rest
        else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}"
    makeConstr fc ((MkBind nm icit x) :: xs) (pat :: pats) =
      if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc
        then do
          rest <- makeConstr fc xs (pat :: pats)
          pure $ (nm, PatWild (getFC pat) icit) :: rest
        else do
          rest <- makeConstr fc xs pats
          pure $ (nm, pat) :: rest

    -- replace constraint with constraints on parameters, or nothing if non-matching clause
    rewriteConstraint : QName -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint))
    rewriteConstraint sctynm vars Nil acc = pure $ Just acc
    rewriteConstraint sctynm vars (c@(nm, y) :: xs) acc =
      if nm == scnm
        then case y of
          PatVar _ _ s => pure $ Just $ c :: (xs ++ acc)
          PatWild _ _ => pure $ Just $ c :: (xs ++ acc)
          -- FIXME why don't we hit this (when user puts 'x' for Just 'x')
          PatLit fc lit => error fc "Literal \{show lit} in constructor split"
          PatCon fc icit nm ys as => if nm == dcName
            then case as of
              Nothing => do
                rest <- makeConstr fc vars ys
                pure $ Just $ rest ++ xs ++ acc
              -- putting this in constraints causes it to be renamed scnm -> nm' when we check body.
              Just nm' => do
                rest <- makeConstr fc vars ys
                pure $ Just $ (scnm, (PatVar fc icit nm')) :: rest ++ xs ++ acc
            else do
              -- TODO can we check this when we make the PatCon?
              top <- get
              case lookup nm top of
                  (Just (MkEntry _ name type (DCon k tcname))) =>
                    if (tcname /= sctynm)
                      then error fc "Constructor is \{show tcname} expected \{show sctynm}"
                      else pure Nothing
                  Just _ => error fc "Internal Error: \{show nm} is not a DCon"
                  Nothing => error fc "Internal Error: DCon \{show nm} not found"
        else rewriteConstraint sctynm vars xs (c :: acc)

    rewriteClause : QName -> List Bind -> Clause -> M (Maybe Clause)
    rewriteClause sctynm vars (MkClause fc cons pats expr) = do
      Just cons <- rewriteConstraint sctynm vars cons Nil | _ => pure Nothing
      pure $ Just $ MkClause fc cons pats expr


splitArgs : Raw -> List (Raw × Icit) -> (Raw × List (Raw × Icit))
splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
splitArgs tm args = (tm, args)


mkPat : (Raw × Icit) -> M Pattern
mkPat (RAs fc as tm, icit) = do

  pat <- mkPat (tm, icit)
  case pat of
    (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
    (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
    t => error fc "Can't put as on non-constructor \{show tm}"
mkPat (tm, icit) = do
  top <- get
  case splitArgs tm Nil of
    ((RVar fc nm), b) => case lookupRaw nm top of
                (Just (MkEntry _ name type (DCon k str))) => do
                  -- TODO check arity, also figure out why we need reverse
                  bpat <- traverse (mkPat) b
                  pure $ PatCon fc icit name bpat Nothing
                -- This fires when a global is shadowed by a pattern var
                -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
                _ => case b of
                                Nil => pure $ PatVar fc icit nm
                                _ => error (getFC tm) "patvar applied to args"
    ((RImplicit fc), Nil) => pure $ PatWild fc icit
    ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments"
    ((RLit fc lit), Nil) => pure $ PatLit fc lit
    ((RLit fc y), b) => error fc "lit cannot be applied to arguments"
    (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}"



makeClause : (Raw × Raw) -> M Clause
makeClause (lhs, rhs) = do
  let (nm, args) = splitArgs lhs Nil
  pats <- traverse mkPat args
  pure $ MkClause (getFC lhs) Nil pats rhs



-- we'll want both check and infer, we're augmenting a context
-- so probably a continuation:
-- Context -> List Decl -> (Context -> M a) -> M a
checkWhere : Context -> List Decl -> Raw -> Val -> M Tm
checkWhere ctx decls body ty = do
  -- we're going to be very proscriptive here
  let (TypeSig sigFC (name :: Nil) rawtype :: decls) = decls
    | x :: _ => error (getFC x) "expected type signature"
    | _ => check ctx body ty
  funTy <- check ctx rawtype (VU sigFC)
  debug $ \ _ => "where clause \{name} : \{rpprint (names ctx) funTy}"
  let (Def defFC name' clauses :: decls') = decls
    | x :: _ => error (getFC x) "expected function definition"
    | _ => error sigFC "expected function definition after this signature"
  unless (name == name') $ \ _ => error defFC "Expected def for \{name}"
  -- REVIEW is this right, cribbed from my top level code
  top <- get
  clauses' <- traverse makeClause clauses
  vty <- eval ctx.env CBN funTy
  debug $ \ _ => "\{name} vty is \{show vty}"
  let ctx' = extend ctx name vty

  -- if I lift, I need to namespace it, add args, and add args when
  -- calling locally
  -- context could hold a Name -> Val (not Tm because levels) to help with that
  -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...)
  -- But I'll attempt letrec first
  tm <- buildTree (withPos ctx' defFC) (MkProb clauses' vty)
  vtm <- eval ctx'.env CBN tm
  -- Should we run the rest with the definition in place?
  -- I'm wondering if switching from bind to define will mess with metas
  -- let ctx' = define ctx name vtm vty
  ty' <- checkWhere ctx' decls' body ty
  pure $ LetRec sigFC name funTy tm ty'

-- checks the body after we're done with a case tree branch
checkDone : Context -> List (String × Pattern) -> Raw -> Val -> M Tm
checkDone ctx Nil body ty = do
  debug $ \ _ => "DONE-> check body \{show body} at \{show ty}"
  -- TODO better dump context function
  debugM $ showCtx ctx
  -- Hack to try to get Combinatory working
  -- we're trying to subst in solutions here.
  env' <- for ctx.env $ \ val => do
    ty <- quote (length' ctx.env) val
    -- This is not getting vars under lambdas
    eval ctx.env CBV ty
  types' <- for ctx.types $ \case
    (nm,ty) =>  do
      nty <- quote (length' env') ty
      ty' <- eval env' CBV nty
      pure (nm, ty')
  let ctx = MkCtx ctx.lvl env' types' ctx.bds ctx.ctxFC
  debug $ \ _ => "AFTER"
  debugM $ showCtx ctx
  -- I'm running an eval here to run case statements that are
  -- unblocked by lets in the env. (Tree.newt:cmp)
  -- The case eval code only works in the Tm -> Val case at the moment.
  -- we don't have anything like `vapp` for case
  ty <- quote (length' ctx.env) ty
  ty <- eval ctx.env CBN ty

  debug $ \ _ => "check at \{show ty}"
  got <- check ctx body ty
  debug $ \ _ => "DONE<- got \{rpprint (names ctx) got}"
  pure got
checkDone ctx ((x, PatWild _ _) :: xs) body ty = checkDone ctx xs body ty
checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty =
  let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC in
  checkDone ctx xs body ty
  where
    rename : List (String × Val) -> List (String × Val)
    rename Nil = Nil
    rename ((name, ty) :: xs) =
      if name == nm
        then (nm', ty) :: xs
        else (name, ty) :: rename xs

checkDone ctx ((x, pat) :: xs) body ty = error (getFC pat) "stray constraint \{x} /? \{show pat}"

-- need to run constructors, then run default

-- wild/var can come before 'x' so we need a list first
getLits : String -> List Clause -> List Literal
getLits nm Nil = Nil
getLits nm ((MkClause fc cons pats expr) :: cs) = case find ((_==_ nm) ∘ fst) cons of
  Just (_, (PatLit _ lit)) => lit :: getLits nm cs
  _ => getLits nm cs

-- collect constructors that are matched on
matchedConstructors : String → List Clause → List QName
matchedConstructors nm Nil = Nil
matchedConstructors nm ((MkClause fc cons pats expr) :: cs) = case find ((_==_ nm) ∘ fst) cons of
  Just (_, (PatCon _ _ dcon _ _)) => dcon :: matchedConstructors nm cs
  _ => matchedConstructors nm cs

-- then build a lit case for each of those

buildLitCase : Context -> Problem -> FC -> String -> Val -> Literal -> M CaseAlt
buildLitCase ctx prob fc scnm scty lit = do

  -- Constrain the scrutinee's variable to be lit value
  let (Just ix) = findIndex' ((_==_ scnm) ∘ fst) ctx.types
    | Nothing => error ctx.ctxFC "\{scnm} not is scope?"
  let lvl = lvl2ix (length' ctx.env) ix
  let scon = (lvl, VLit fc lit)
  ctx' <- updateContext ctx (scon :: Nil)
  let clauses = mapMaybe rewriteClause prob.clauses

  when (length' clauses == 0) $ \ _ => error ctx.ctxFC "Missing case for \{show lit} splitting \{scnm}"
  tm <- buildTree ctx' (MkProb clauses prob.ty)
  pure $ CaseLit lit tm

  where
    -- FIXME - thread in M for errors
    -- replace constraint with constraints on parameters, or nothing if non-matching clause
    rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint)
    rewriteConstraint Nil acc = Just acc
    rewriteConstraint (c@(nm, y) :: xs) acc =
      if nm == scnm
        then case y of
          PatVar _ _ s => Just $ c :: (xs ++ acc)
          PatWild _ _ => Just $ c :: (xs ++ acc)
          PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing
          PatCon _ _ str ys as => Nothing -- error matching lit against constructor
        else rewriteConstraint xs (c :: acc)

    rewriteClause : Clause -> Maybe Clause
    rewriteClause (MkClause fc cons pats expr) = do
      cons <- rewriteConstraint cons Nil
      pure $ MkClause fc cons pats expr

buildDefault : Context → Problem → FC → String → M CaseAlt
buildDefault ctx prob fc scnm = do
  let defclauses = filter isDefault prob.clauses
  when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}"
  CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty)
  where
    isDefault : Clause -> Bool
    isDefault cl = case find ((_==_ scnm) ∘ fst) cl.cons of
      Just (_, (PatVar _ _ _)) => True
      Just (_, (PatWild _ _)) => True
      Nothing => True
      _ => False

buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt)
buildLitCases ctx prob fc scnm scty = do
  let lits = nub $ getLits scnm prob.clauses
  alts <- traverse (buildLitCase ctx prob fc scnm scty) lits
  -- TODO build default case
  -- run getLits
  -- buildLitCase for each

  let defclauses = filter isDefault prob.clauses
  when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}"
  tm <- buildTree ctx (MkProb defclauses prob.ty)

  pure $ alts ++ ( CaseDefault tm  :: Nil)
  where
    isDefault : Clause -> Bool
    isDefault cl = case find ((_==_ scnm) ∘ fst) cl.cons of
      Just (_, (PatVar _ _ _)) => True
      Just (_, (PatWild _ _)) => True
      Nothing => True
      _ => False

-- TODO - figure out if these need to be in Prelude or have a special namespace
-- If we lookupRaw "String", we could get different answers in different contexts.
-- maybe Hardwire this one
stringType intType charType : QName
stringType = QN ("Prim" :: Nil) "String"
intType = QN ("Prim" :: Nil) "Int"
charType = QN ("Prim" :: Nil) "Char"

litTyName : Literal -> QName
litTyName (LString str) = stringType
litTyName (LInt i) = intType
litTyName (LChar c) = charType

renameContext : String -> String -> Context -> Context
renameContext from to ctx = MkCtx ctx.lvl ctx.env (go ctx.types) ctx.bds ctx.ctxFC
  where
    go : List (String × Val) -> List (String × Val)
    go Nil = Nil
    go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types

-- This process is similar to extendPi, but we need to stop
-- if one clause is short on patterns.
buildTree ctx (MkProb Nil ty) = error emptyFC "no clauses"
buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit rig a b)) = do
  let l = length' ctx.env
  let nm = fresh str -- "pat"
  let ctx' = extend ctx nm a
  -- type of the rest
  clauses <- traverse (introClause nm icit) prob.clauses
  -- REVIEW fc from a pat?
  vb <- b $$ VVar fc l Lin
  Lam fc nm icit rig <$> buildTree ctx' (MkProb clauses vb)
buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) =
  error fc "Extra pattern variables \{show pats}"
-- need to find some name we can split in (x :: xs)
-- so LHS of constraint is name (or VVar - if we do Val)
-- then run the split
-- some of this is copied into check
buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do
  debug $ \ _ => "buildTree \{show constraints} \{show expr}"
  let (Just (scnm, pat)) = findSplit constraints
    | _ => do
      debug $ \ _ => "checkDone \{show constraints}"
      checkDone ctx constraints expr ty

  debug $ \ _ => "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}"
  let (Just (sctm, scty)) = lookupName ctx scnm
    | _ => error fc "Internal Error: can't find \{scnm} in environment"

  -- REVIEW We probably need to know this is a VRef before we decide to split on this slot..
  scty' <- unlet ctx.env scty >>= forceType ctx.env
  -- TODO attempting to pick up Autos that could have been solved immediately
  -- If we try on creation, we're looping at the moment, because of the possibility
  -- of Ord a -> Ord b -> Ord (a \x b). Need to cut earlier when solving or switch to
  -- Idris method...
  scty' <- case scty' of
    (VMeta fc1 ix sp) => do
      meta <- lookupMeta ix
      case meta of
        (Solved _ k t) => forceType ctx.env scty'
        (Unsolved _ k xs _ _ _) => do
          top <- get
          mc <- readIORef top.metaCtx
          -- TODO - only hit the relevant ones
          ignore $ solveAutos 0
          forceType ctx.env scty'
        OutOfScope => pure scty'

    _ => pure scty'

  case pat of
    PatCon fc _ _ _ as => do
      -- expand vars that may be solved, eval top level functions
      debug $ \ _ => "EXP \{show scty} -> \{show scty'}"
      -- this is per the paper, but it would be nice to coalesce
      -- default cases
      cons <- getConstructors ctx (getFC pat) scty'
      let matched = matchedConstructors scnm prob.clauses
      let (hit,miss) = partition (flip elem matched ∘ fst) cons
      -- need to check miss is possible
      miss' <- filterM (checkCase ctx prob scnm scty') miss

      debug $ \ _ => "CONS \{show $ map fst cons} matched \{show matched} miss \{show miss} miss' \{show miss'}"

      -- process constructors with matches
      alts <- traverse (buildCase ctx prob scnm scty') hit
      debug $ \ _ => "GOTALTS \{show alts}"
      let alts' = mapMaybe id alts
      when (length' alts' == 0) $ \ _ => error (fc) "no alts for \{show scty'}"
      -- build a default case for missed constructors
      case miss' of
        Nil => pure $ Case fc sctm (mapMaybe id alts)
        _ => do
        -- ctx prob fc scnm
          default <- buildDefault ctx prob fc scnm
          pure $ Case fc sctm (snoc alts' default)

    PatLit fc v => do
      let tyname = litTyName v
      case scty' of
        (VRef fc1 nm sp) => when (nm /= tyname) $ \ _ => error fc "expected \{show scty} and got \{show tyname}"
        _ => error fc "expected \{show scty} and got \{show tyname}"
      -- need to run through all of the PatLits in this slot and then find a fallback
      -- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't
      alts <- buildLitCases ctx prob fc scnm scty
      pure $ Case fc sctm alts
    pat => error (getFC pat) "Internal error - tried to split on \{show pat}"

showDef : Context -> List String -> Int -> Val -> M String
showDef ctx names n v@(VVar _ n' Lin) =  if n == n'
  then pure ""
  else do
    -- REVIEW - was using names, is it ok to pull from the context?
    vv <- vprint ctx v
    pure "= \{vv}"
showDef ctx names n v = do
  vv <- vprint ctx v
  pure "= \{vv}"
  -- pure "= \{rpprint names !(quote ctx.lvl v)}"

-- desugar do
undo : FC -> List DoStmt -> M Raw
undo prev Nil = error prev "do block must end in expression"
undo prev ((DoExpr fc tm) :: Nil) = pure tm
-- TODO decide if we want to use >> or just >>=
undo prev ((DoExpr fc tm) :: xs) = do
  xs' <- undo fc xs
  pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs
undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
  top <- get
  case lookupRaw nm top of
    Just _ => do
      let nm = "$sc"
      xs' <- undo fc xs
      rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: Nil)
      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
        (RLam fc (BI fc nm Explicit Many) rest) Explicit
    Nothing => do
      xs' <- undo fc xs
      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
        (RLam fc (BI fc' nm Explicit Many) xs') Explicit
undo prev ((DoArrow fc left right alts) :: xs) = do
  let nm = "$sc"
  xs' <- undo fc xs
  rest <- pure $ RCase fc (RVar fc nm) (MkAlt left xs' :: alts)
  pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
    (RLam fc (BI fc nm Explicit Many) rest) Explicit

check ctx tm ty = do
  ty' <- forceType ctx.env ty
  case (tm, ty') of
    (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
    (RIf fc a b c, ty) =>
      let tm' = RCase fc a ( MkAlt (RVar (getFC b) "True") b :: MkAlt (RVar (getFC c) "False") c  :: Nil) in
      check ctx tm' ty
    (RDo fc stmts, ty) => do
      stmts' <- undo fc stmts
      check ctx stmts' ty
    (RCase fc rsc alts, ty) => do
      (sc, scty) <- infer ctx rsc
      scty <- forceMeta scty
      debug $ \ _ => "SCTM \{rpprint (names ctx) sc}"
      debug $ \ _ => "SCTY \{show scty}"

      let scnm = fresh "sc"
      top <- get
      clauses <- for alts $ \case
        (MkAlt pat rawRHS) => do
          pat' <- mkPat (pat, Explicit)
          pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS
      -- buildCase expects scrutinee to be a name in the context, so we need to let it.
      -- if it's a Bnd and not shadowed we could skip the let, but that's messy.
      let ctx' = withPos (extend ctx scnm scty) (getFC tm)
      tree <- buildTree ctx' $ MkProb clauses ty
      pure $ Let fc scnm sc tree

    -- rendered in ProcessDecl
    (RHole fc, ty) => freshMeta ctx fc ty User

    (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' rig a b)) => do
            debug $ \ _ => "icits \{nm} \{show icit} \{nm'} \{show icit'}"
            if icit == icit' then do
                let var = VVar fc (length' ctx.env) Lin
                let ctx' = extend ctx nm a
                bapp <- b $$ var
                tm' <- check ctx' tm bapp
                pure $ Lam fc nm icit rig tm'
              else if icit' /= Explicit then do
                let var = VVar fc (length' ctx.env) Lin
                ty' <- b $$ var
                -- use nm' here if we want them automatically in scope
                sc <- check (extend ctx nm' a) t ty'
                pure $ Lam fc nm' icit rig sc
              else
                error fc "Icity issue checking \{show t} at \{show ty}"
    (t@(RLam _ (BI fc nm icit quant) tm), ty) => do
              pty <- prvalCtx ty
              error fc "Expected pi type, got \{pty}"


    (RLet fc nm ty v sc, rty) => do
      ty' <- check ctx ty (VU emptyFC)
      vty <- eval ctx.env CBN ty'
      v' <- check ctx v vty
      vv <- eval ctx.env CBN v'
      let ctx' = define ctx nm vv vty
      sc' <- check ctx' sc rty
      pure $ Let fc nm v' sc'

    (RImplicit fc, ty) => freshMeta ctx fc ty Normal

    (tm, ty@(VPi fc nm' Implicit rig a b)) => do
      let names = map fst ctx.types
      debug $ \ _ => "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
      let var = VVar fc (length' ctx.env) Lin
      ty' <- b $$ var
      debugM $ do
        pty' <- prvalCtx {{(extend ctx nm' a)}} ty'
        pure "XXX ty' is \{pty'}"
      sc <- check (extend ctx nm' a) tm ty'
      pure $ Lam (getFC tm) nm' Implicit rig sc

    (tm, ty@(VPi fc nm' Auto rig a b)) => do
      let names = map fst ctx.types
      debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} "
      let var = VVar fc (length' ctx.env) Lin
      ty' <- b $$ var
      debugM $ do
        pty' <- prvalCtx {{(extend ctx nm' a)}} ty'
        pure "XXX ty' is \{pty'}"
      sc <- check (extend ctx nm' a) tm ty'
      pure $ Lam (getFC tm) nm' Auto rig sc

    (tm,ty) => do
      (tm', ty') <- infer ctx tm
      (tm', ty') <- insert ctx tm' ty'

      let names = map fst ctx.types
      debug $ \ _ => "INFER \{show tm} to (\{rpprint names tm'} : \{show ty'}) expect \{show ty}"
      unifyCatch (getFC tm) ctx ty' ty
      pure tm'

infer ctx (RVar fc nm) = go 0 ctx.types
  where
    go : Int -> List (String × Val)  -> M (Tm × Val)
    go i Nil = do
      top <- get
      case lookupRaw nm top of
        Just (MkEntry _ name ty def) => do
          debug $ \ _ => "lookup \{show name} as \{show def}"
          vty <- eval Nil CBN ty
          pure (Ref fc name, vty)
        Nothing => error fc "\{show nm} not in scope"
    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty)
      else go (i + 1) xs

infer ctx (RApp fc t u icit) = do
  -- If the app is explicit, add any necessary metas
  (icit, t, tty) <- case the Icit icit of
      Explicit => do
        (t, tty) <- infer ctx t
        (t, tty) <- insert ctx t tty
        pure (Explicit, t, tty)
      Implicit => do
        (t, tty) <- infer ctx t
        pure (Implicit, t, tty)
      Auto => do
        (t, tty) <- infer ctx t
        pure (Auto, t, tty)

  (a,b) <- do
    tty' <- forceMeta tty
    case tty' of
      (VPi fc' str icit' rig a b) => if icit' == icit then pure (a,b)
          else error fc "IcitMismatch \{show icit} \{show icit'}"

      -- If it's not a VPi, try to unify it with a VPi
      -- TODO test case to cover this.
      tty => do
        debug $ \ _ => "unify PI for \{show tty}"
        a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN
        b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal
        -- FIXME - I had to guess Many here.  What are the side effects?
        unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b)
        pure (a,b)

  u <- check ctx u a
  u' <- eval ctx.env CBN u
  bappu <- b $$ u'
  pure (App fc t u, bappu)

infer ctx (RU fc) = pure (UU fc, VU fc) -- YOLO
infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do
  ty' <- check ctx ty (VU fc)
  vty' <- eval ctx.env CBN ty'
  ty2' <- check (extend ctx nm vty') ty2 (VU fc)
  pure (Pi fc nm icit quant ty' ty2', (VU fc))
infer ctx (RLet fc nm ty v sc) = do
  ty' <- check ctx ty (VU emptyFC)
  vty <- eval ctx.env CBN ty'
  v' <- check ctx v vty
  vv <- eval ctx.env CBN v'
  let ctx' = define ctx nm vv vty
  (sc',scty) <- infer ctx' sc
  pure $ (Let fc nm v' sc', scty)

infer ctx (RAnn fc tm rty) = do
  ty <- check ctx rty (VU fc)
  vty <- eval ctx.env CBN ty
  tm <- check ctx tm vty
  pure (tm, vty)

infer ctx (RLam _ (BI fc nm icit quant) tm) = do
  a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN
  let ctx' = extend ctx nm a
  (tm', b) <- infer ctx' tm
  debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}"
  tyb <- quote (1 + ctx.lvl) b
  pure $ (Lam fc nm icit quant tm', VPi fc nm icit quant a (MkClosure ctx.env tyb))

infer ctx (RImplicit fc) = do
  ty <- freshMeta ctx fc (VU emptyFC) Normal
  vty <- eval ctx.env CBN ty
  tm <- freshMeta ctx fc vty Normal
  pure (tm, vty)

infer ctx (RLit fc (LString str)) = do
  ty <- primType fc stringType
  pure (Lit fc (LString str), ty)
infer ctx (RLit fc (LInt i)) = do
  ty <- primType fc intType
  pure (Lit fc (LInt i), ty)
infer ctx (RLit fc (LChar c)) = do
  ty <- primType fc charType
  pure (Lit fc (LChar c), ty)
infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns"
infer ctx tm = error (getFC tm) "Implement infer \{show tm}"