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
import Lib.Syntax
import Lib.Types
import Lib.Error

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 ((FunDef fc nm cl) :: rest@(FunDef _ nm' cl' :: xs)) =
  if nm == nm' then collectDecl (FunDef fc nm (cl ++ cl') :: xs)
  else (FunDef fc nm cl :: collectDecl rest)
collectDecl (x :: xs) = x :: collectDecl xs

-- TODO Move this, so we don't need to import all of Elab
rpprint : List String → Tm → String
rpprint names tm = render 90 $ pprint names tm

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 (reverse $ 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

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
instance Show UnifyMode where
  show UNormal = "UNormal"
  show UPattern = "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

setMetaMode : MetaMode → M Unit
-- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst
setMetaMode mcmode = modifyTop [ currentMod $= [modMetaCtx $= [mcmode := mcmode] ] ]

setMetaContext : MetaContext → M Unit
setMetaContext mc = modifyTop [ currentMod $= [ modMetaCtx := mc ]]

findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
findMatches ctx ty Nil = pure Nil
findMatches ctx ty ((name, type) :: xs) = do
  let (True) = isCandidate ty type
    | False => findMatches ctx ty xs

  top <- getTop
  -- save context
  let mc = top.currentMod.modMetaCtx
  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
      let (QN ns nm) = name
      let (cod, tele) = splitTele type
      setMetaMode CheckFirst
      tm <- check ctx (RVar fc nm) ty
      debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
      setMetaContext mc
      (_::_ name) <$> findMatches ctx ty xs)
    (\ err => do
      debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}"
      setMetaContext 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 <- getTop
      let mc = top.currentMod.modMetaCtx
      catchError(do
          debug $ \ _ => "TRY context \{nm} : \{rpprint (names ctx) type} for \{show ty}"
          unifyCatch (getFC ty) ctx ty vty
          let mc' = top.currentMod.modMetaCtx
          setMetaContext mc
          tm <- quote ctx.lvl tm
          (_::_ (tm, vty)) <$> go xs)
        (\ err => do
          debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}"
          setMetaContext mc
          go xs)

getArity : Tm -> List Quant
getArity (Pi x str icit rig t u) = rig :: getArity u
-- Ref or App (of type constructor) are valid
getArity _ = Nil

-- 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 x
      debug $ \ _ => "AUTO ---> \{show ty}"
      -- we want the context here too.
      top <- getTop
      Nil <- contextMatches ctx ty
          | ((tm, vty) :: Nil) => do
              val <- eval ctx.env tm
              debug $ \ _ => "LOCAL SOLUTION \{rpprint Nil tm} evaled to \{show val}"
              let sp = makeSpine ctx.lvl ctx.bds
              solve ctx.env k sp val
              debug $ \ _ => "<-- AUTO LOCAL"
              debug $ \ _ => ">UNIFY \{show k}"
              -- Causes infinite loop if we do this before the solve
              -- may be nice to push it into solve, but vty is not there..
              unifyCatch (getFC ty) ctx ty vty
              debug $ \ _ => "<UNIFY \{show k}"
              pure True
          | res => do
              debug $ \ _ => "LOCAL FAILED to solve \{show ty}, matches: \{render 90 $ commaSep $ map (pprint Nil ∘ fst) res}"
              pure False

      let (VRef _ tyname _) = ty | _ => pure False
      let cands = fromMaybe Nil $ lookupMap' tyname top.hints
      (QN _ nm :: Nil) <- findMatches ctx ty cands
        | res => do
          debug $ \ _ => "GLOBAL FAILED to solve \{show ty}, matches: \{show res}"
          pure False
      -- The `check` fills in implicits
      tm <- check ctx (RVar fc nm) ty
      val <- eval ctx.env tm
      debug $ \ _ => "SOLUTION \{rpprint Nil tm} evaled to \{show val}"
      debug $ \ _ => "GLOBAL SOLUTION \{show val}"
      let sp = makeSpine ctx.lvl ctx.bds
      -- Sometimes this gets solved during the `check` above
      entry@(Unsolved _ _ _ _ _ _) <- lookupMeta k | _ => pure True
      solve ctx.env k sp val
      pure True
trySolveAuto _ = pure False

solveAutos : M Unit
solveAutos = do
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  let autos = filter isAuto $ mapMaybe (flip lookupMap' mc.metas) mc.autos
  res <- run autos
  -- If anything is solved, we try again from the top
  if res then solveAutos 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

updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit
updateMeta ix f = do
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit
  me <- f me
  let autos = case me of
    Solved _ _ _ => filter (_/=_ ix) mc.autos
    _ => mc.autos
  setMetaContext $ [metas $= updateMap ix me; autos := autos] mc

-- Try to solve autos that reference the meta ix
checkAutos : QName -> List QName -> M Unit
checkAutos ix Nil = pure MkUnit
checkAutos ix (cand :: rest) = do
  entry@(Unsolved fc k ctx ty AutoSolve _) <- lookupMeta cand | _ => checkAutos ix rest
  case ty of
    VRef _ nm sp => if checkMeta sp
        then trySolveAuto entry >> checkAutos ix rest
        else pure MkUnit
    _ => pure MkUnit
  checkAutos ix rest
  where
    checkMeta : SnocList Val → Bool
    checkMeta Lin = False
    checkMeta (sp :< VMeta _ nm _) = if nm == ix then True else checkMeta sp
    checkMeta (sp :< _) = checkMeta sp

checkAutos ix (_ :: rest) = checkAutos ix rest

addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit
addConstraint env ix sp tm = do
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  let (CheckAll) = mc.mcmode | _ => pure MkUnit
  updateMeta ix $ \case
    (Unsolved pos k a b c cons) => do
      debug $ \ _ => "Add constraint \{show ix} \{show sp} =?= \{show tm}"
      pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
    (Solved fc k tm) => error fc "Meta \{show k} already solved [addConstraint]"
    (OutOfScope) => error' "Meta \{show ix} out of scope"

-- 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 (getFC v) "non-variable in pattern \{show v}"

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)

-- run action if mcmode allows it, ratcheting as necessary
maybeCheck : M Unit -> M Unit
maybeCheck action = do
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  case mc.mcmode of
    CheckAll => action
    CheckFirst => do
      setMetaMode NoCheck
      action
      setMetaMode 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 \{show ix} \{show sp} =?= \{show t}"
      addConstraint env m sp t
  let l = length' env
  debug $ \ _ => "meta \{show meta}"

  -- tests/UnifyPi.newt - Solution is non-linear, but is solved later
  -- REVIEW We add constraints to be checked later (here and above) and assume the unification succeeds
  -- Will this get is into trouble?
  Right ren <- tryError $ invert l sp
    | Left err => do
        debug $ \ _ => "postpone constraint \{showError "" err}"
        addConstraint env m sp t
  -- force unlet
  hack <- quote l t
  t <- eval env hack
  catchError (do
    tm <- rename m ren l t

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

    updateMeta m $ \case
      (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
      (Solved fc k x) => error fc "Meta \{show ix} already solved! [solve2]"
      OutOfScope => error' "Meta \{show ix} out of scope"
    maybeCheck $ do
      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
      -- check any autos
      top <- getTop
      let mc = top.currentMod.modMetaCtx
      let (CheckAll) = mc.mcmode | _ => pure MkUnit
      debug $ \ _ => "check autos depending on \{show ix} \{debugStr mc.mcmode}"
      checkAutos ix mc.autos
    pure MkUnit
    )

    (\case
      Postpone fc ix msg => do
        -- let someone else solve this and then check again.
        debug $ \ _ => "CONSTRAINT2 \{show ix} \{show sp} =?= \{show t}"
        addConstraint env m sp t
      -- replace with wrapper
      err => throwError (E (getFC err) "\{errorMsg err} for \{show ix} \{show sp} =?= \{show 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'

    -- TODO adds about 2kb, maybe add one more func for unifyPi?
    -- or rearrange to split on first arg and then case on second (might be a good experiment)
    unifyRest (VLit fc l) (VLit _ k) = if l == k
      then pure neutral
      else error fc "unify failed \{show l} =?= \{show k}"

    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') = do
      -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y
      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'}"

    unifyRef t         u@(VRef fc' k' sp') = do
      debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
      top <- getTop
      case lookup k' top of
        Just (MkEntry _ name ty (Fn tm) _) => do
          vtm <- eval Nil tm
          appvtm <- vappSpine vtm sp'
          unify env mode t appvtm
        _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]"

    unifyRef t@(VRef fc k sp) u = do
      debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
      top <- getTop
      case lookup k top of
        Just (MkEntry _ name ty (Fn tm) _) => do
          vtm <- eval Nil tm
          tmsp <- vappSpine vtm sp
          unify env mode tmsp u
        _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}"
    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'
      -- FIXME - get some names in here.
      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)
        (Lin,_) => pure $ MkResult ((k, u') :: Nil)
        (_,Lin) => pure $ MkResult ((k', t') :: Nil)
        _ => error fc "Failed to unify \{show t'} and \{show u'} at \{show mode}"

    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 <- getTop
  let mc = top.currentMod.modMetaCtx
  debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
  -- need the ns here
  -- we were fudging this for v1
  let qn = QN top.currentMod.modName "$m\{show mc.next}"
  let newmeta = Unsolved fc qn ctx ty kind Nil
  let autos = case kind of
      AutoSolve => qn :: mc.autos
      _ => mc.autos
  setMetaContext $ [ metas $= updateMap qn newmeta; autos := autos; next $= 1 +] mc

  -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
  pure $ applyBDs 0 (Meta fc qn) ctx.bds
  where
    applyBDs : Int -> Tm -> List BD -> Tm
    applyBDs k t Nil = t
    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 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 m
      bapp <- b $$ mv
      insert ctx (App (getFC tm) tm m) bapp
    va => pure (tm, va)

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 as a Tm
buildTree : Context -> Problem -> M Tm

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

-- Find the next constraint to split on
-- We go in order at the moment, which happens to be right to left
-- FIXME we should skip ones with non-TCon types, hoping we'll have more information after
-- solving the others.
-- TODO If the type is a meta and we're looking at a DCon, we _could_ give the TCon some
-- args and try to solve the meta, but I'm not sure if that's a good idea.
findSplit : List Constraint -> Maybe Constraint
findSplit Nil = Nothing
findSplit (x@(PC nm (PatCon _ _ _ _ _) _) :: xs) = Just x
findSplit (x@(PC nm (PatLit _ val) _) :: xs) = Just x
findSplit (x :: xs) = findSplit xs

lookupDCon : QName -> M (QName × Int × Tm)
lookupDCon nm = do
  top <- getTop
  case lookup nm top of
    (Just (MkEntry _ name type (DCon _ _ k str) _)) => pure (name, length' k, type)
    Just _ => error emptyFC "Internal Error: \{show nm} is not a DCon"
    Nothing => error emptyFC "Internal Error: DCon \{show nm} not found"

-- Get the constructors for a type
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 <- getTop
      case lookup nm top of
        (Just (MkEntry _ name type (TCon _ names) _)) => pure names
        _ => error scfc "Not a type constructor: \{show nm}"

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 is the telescope of a constructor
-- return context, remaining type, and list of names
-- So Γ |- (a : A) -> (b : B) -> C  --> Γ, (a : A), (b : B) |- C[fresh_a/a,fresh_b/b] and "fresh_a", "fresh_b"
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

-- Update context when a variable is constrained to a value.
-- For now, we're updating the context to turn var bindings
-- into lets.
-- TODO rework this to do something better.
updateContext : Context -> List (Int × Val) -> M Context
updateContext ctx Nil = pure ctx
updateContext ctx ((k, val) :: cs) =
  -- We were turning Bound into Defined
  if isSelf k val then updateContext ctx cs
  else
  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"
  where
    isSelf : Int → Val → Bool
    isSelf ix (VVar _ k Lin) = ix == k
    isSelf ix _ = False

    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

-- check if a constructor is possible. Used to check impossible and missing cases.
checkCase : Context → String → Val → (QName × Int × Tm) → M Bool
checkCase ctx scnm scty (dcName, arity, ty) = do
  vty <- eval Nil ty
  (ctx', ty', vars, sc) <- extendPi ctx (vty) Lin Lin
  (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

-- Build the tree for a match against a casealt `dcName`
-- return Nothing if dcon type 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}"
  -- Add the constructor arguments to the context
  vty <- eval Nil 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 constructor's
  -- 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
    -- value is dotted
    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}"

        -- constrain arguments to spine of dotted value
        let lvl = length' ctx'.env - length' vars
        let scons = constrainSpine lvl (sp <>> Nil)
        ctx' <- updateContext ctx' scons

        -- TODO bundle up this debug message so it doesn't run the loops when not debugging
        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}"
            putStrLn "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 Constraint)
    makeConstr fc Nil Nil = pure $ Nil
    makeConstr fc Nil (pat :: pats) = error (getFC pat) "too many patterns"

    makeConstr fc ((MkBind nm Implicit ty) :: xs) Nil  = do
      rest <- makeConstr fc xs Nil
      pure $ PC nm (PatWild emptyFC Implicit) ty :: rest
    makeConstr fc ((MkBind nm Auto ty) :: xs) Nil = do
      rest <- makeConstr fc xs Nil
      pure $ PC nm (PatWild emptyFC Auto) ty :: rest
    makeConstr fc ((MkBind nm Explicit ty) :: xs) Nil = error fc "not enough patterns"
    makeConstr fc ((MkBind nm Explicit ty) :: xs) (pat :: pats) =
      if getIcit pat == Explicit
        then do
          rest <- makeConstr fc xs pats
          pure $ PC nm pat ty :: rest
        else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}"
    makeConstr fc ((MkBind nm icit ty) :: xs) (pat :: pats) =
      if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc
        then do
          rest <- makeConstr fc xs (pat :: pats)
          pure $ PC nm (PatWild (getFC pat) icit) ty :: rest
        else do
          rest <- makeConstr fc xs pats
          pure $ PC nm pat ty :: rest

    -- constraints on scnm with constraints on parameters, or nothing if non-matching clause
    -- TODO update types that reference the scrutinee?
    rewriteConstraint : QName -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint))
    rewriteConstraint sctynm vars Nil acc = pure $ Just acc
    rewriteConstraint sctynm vars (c@(PC nm y scty) :: xs) acc =
      if nm == scnm
        then case y of
          PatVar _ _ s => pure $ Just $ c :: (xs ++ acc)
          PatImpossible _ => pure $ Just $ c :: (xs ++ acc)
          PatWild _ _ => pure $ Just $ c :: (xs ++ acc)
          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 $ (PC scnm (PatVar fc icit nm') scty) :: rest ++ xs ++ acc
            else do
              -- TODO can we check this when we make the PatCon?
              top <- getTop
              case lookup nm top of
                  (Just (MkEntry _ name type (DCon _ _ k tcname) _)) =>
                    if (tcname /= sctynm)
                      then error fc "Constructor is a \{show tcname} expected a \{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 <- getTop
  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 (getFC tm) 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"
                _ => if isUpperName nm
                        -- This is not entirely accurate - it could be a function def
                        then error (getFC tm) "\{nm} not in scope"
                        else 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
    ((RImpossible fc), _) => pure $ PatImpossible fc
    ((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 × Maybe 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, no forward declaration
  -- need multiple defs in letrec if we want to loosen this
  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 (FunDef 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 <- getTop
  clauses' <- traverse makeClause clauses
  vty <- eval ctx.env 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 tm
  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 : FC -> Context -> List Constraint -> Maybe Raw -> Val -> M Tm
checkDone fc ctx Nil Nothing ty = error fc "impossible clause needs () on RHS"
checkDone fc ctx Nil (Just 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 ty
  types' <- for ctx.types $ \case
    (nm,ty) =>  do
      nty <- quote (length' env') ty
      ty' <- eval env' 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 ty

  debug $ \ _ => "check at \{show ty}"
  got <- check ctx body ty
  debug $ \ _ => "DONE<- got \{rpprint (names ctx) got}"
  pure got
checkDone fc ctx (PC x (PatWild pvfc icit) scty :: xs) body ty = do
  -- sometimes have the same FC as real arguments
  when (icit == Explicit) $ \ _ => addInfo $ CaseSplit pvfc ctx "_" scty
  checkDone fc ctx xs body ty
checkDone fc ctx (PC nm (PatVar pvfc _ nm') scty :: xs) body ty = do
  -- TIME 5.50 -> 5.62 (we can flag this if it's an issue)
  addInfo $ CaseSplit pvfc ctx nm' scty

  let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC
  checkDone fc 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

-- I'm running this at the end to ensure everything relevant has been split
-- if we have `foo Z ()`, we want to be sure `Z` was matched before we check
-- there are no possible constructors for the second place.
checkDone fc ctx (PC nm (PatImpossible fc') scty :: xs) body ty = do
  -- FIXME check impossible - We need a scrutinee type here!
  -- I think we want it anyway in those constraints

  cons <- getConstructors ctx fc scty
  Nil <- filterM (checkCase ctx nm scty) cons
    | xs => error fc' "possible constructors: \{show $ map fst xs}"
  pure $ Erased fc

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

-- need to run constructors, then run default

matchName : String → Constraint → Bool
matchName nm (PC n _ scty) = nm == n

isDefaultCase : String -> Clause -> Bool
isDefaultCase scnm cl = case find (matchName scnm) cl.cons of
  Just (PC _ (PatVar _ _ _) _) => True
  Just (PC _ (PatWild _ _) _) => True
  Nothing => True
  _ => False

-- FIXME - ty is in the clause now.
-- wild/var can come before 'x' so we need a list first
getLits : Val -> String -> List Clause -> M (List Literal)
getLits ty nm Nil = pure Nil
getLits ty nm ((MkClause fc cons pats expr) :: cs) = case find (matchName nm) cons of
  Just (PC _ (PatLit _ lit) _) => _::_ lit <$> getLits ty nm cs
  Just (PC _ (PatCon fc _ _ _ _) _) => error fc "expected \{show ty}"
  _ => getLits ty nm cs

-- collect constructors that are matched on
matchedConstructors : String → List Clause → List (FC × QName)
matchedConstructors nm Nil = Nil
matchedConstructors nm ((MkClause fc cons pats expr) :: cs) = case find (matchName nm) cons of
  Just (PC _ (PatCon fc _ dcon _ _) _) => (fc, 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@(PC nm y scty) :: xs) acc =
      if nm == scnm
        then case y of
          PatVar _ _ s => Just $ c :: (xs ++ acc)
          (PatImpossible _) => 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 → List QName → M CaseAlt
buildDefault ctx prob fc scnm missing = do
  let defclauses = filter (isDefaultCase scnm) prob.clauses
  case defclauses of
    Nil => do
      addInfo $ MissingCases fc ctx missing
      addError $ E fc "missing cases: \{show missing}"
      hole <- freshMeta ctx fc prob.ty ErrorHole
      pure $ CaseDefault hole
    _ => CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty)

buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt)
buildLitCases ctx prob fc scnm scty = do
  lits <- nub <$> getLits scty scnm prob.clauses
  alts <- traverse (buildLitCase ctx prob fc scnm scty) lits

  let defclauses = filter (isDefaultCase scnm) 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)

-- Names of builtin primitive types, declared in Main.newt
stringType intType charType boolType : QName
stringType = QN primNS "String"
intType = QN primNS "Int"
charType = QN primNS "Char"
boolType = QN primNS "Bool"

litTyName : Literal -> QName
litTyName (LString str) = stringType
litTyName (LInt i) = intType
litTyName (LChar c) = charType
litTyName (LBool _) = boolType -- not used

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

checkDups : FC → List Constraint → M Unit
checkDups fc = go Nil
  where
    go : List String → List Constraint → M Unit
    go seen Nil = pure MkUnit
    go seen (PC nm _ _ :: cons) =
      if elem nm seen
        then error fc "Duplicate name \{show nm}"
        else go (nm :: seen) cons

-- 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 a) 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 (PC scnm pat scty)) = findSplit constraints
    | _ => do
      debug $ \ _ => "checkDone \{show constraints}"
      checkDups fc constraints
      checkDone fc 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...
  -- This is necessary for tests/InferenceIssue.newt
  -- solveAutos below is the important part
  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
          -- TODO - only check the relevant autos
          solveAutos
          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 matched' = map snd matched
      let (hit,miss) = partition (flip elem matched' ∘ fst) cons
      -- need to check miss is possible
      miss' <- filterM (checkCase ctx scnm scty') miss
      for matched $ \case
       (fc, qn) => do
          if elem qn (map fst cons)
            then pure MkUnit
            else error fc "\{show qn} not a constructor for \{show scty}"

      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)
        missed => do
        -- ctx prob fc scnm
          default <- buildDefault ctx prob fc scnm (map fst missed)
          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}"

-- desugar do
undo : List DoStmt -> M Raw
-- Should be unreachable in practice
undo Nil = error emptyFC "do block must end in expression"
undo ((DoExpr fc tm) :: Nil) = pure tm
undo (tm :: Nil) = error (getFC tm) "do block must end in expression"
undo ((DoExpr fc tm) :: xs) = do
  xs' <- undo xs
  -- Not sure if it helps inference or not (and now fails with erasure thing)
  -- pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) xs' Explicit
  pure $ RApp fc (RApp fc (RVar fc "bind") tm Explicit) (RLam fc (BI fc "_" Explicit Many) xs') Explicit
undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
undo ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
  top <- getTop
  case lookupRaw nm top of
    Just _ => do
      let nm = "$sc"
      xs' <- undo xs
      rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: Nil)
      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
        (RLam fc (BI fc nm Explicit Many) rest) Explicit
    Nothing => do
      xs' <- undo xs
      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
        (RLam fc (BI fc' nm Explicit Many) xs') Explicit
undo ((DoArrow fc left right alts) :: xs) = do
  let nm = "$sc"
  xs' <- undo xs
  rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: alts)
  pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
    (RLam fc (BI fc nm Explicit Many) rest) Explicit


-- REVIEW should `arg` be assigned to a variable with `RLet`?
-- REVIEW a case statement to destruct the record instead of projections
-- would make less work for the compiler / inliner.

-- updateRec makes a list of fields and a term for the current value (collect), swaps in
-- any updates present in the code (doClause), and generates an application of the
-- constructor.
updateRec : Context → FC → List UpdateClause → Maybe Raw → Val → M Tm
updateRec ctx fc clauses arg ty = do
  ((QN _ conname), args) <- getTele arg ty
  args' <- foldlM doClause args clauses
  let tm = foldl (\ acc tm => RApp (getFC tm) acc tm Explicit) (RVar fc conname) $ map snd args'
  let tm = case arg of
    Just arg => tm
    Nothing => RLam fc (BI fc "$ru" Explicit Many) tm
  check ctx tm ty
  where
    app : FC → Raw → Raw → Raw
    -- A nested recored update ended up as an RApp of a bare update, essentially
    -- a beta redux, and it hit `infer` on the RUpdateRec
    app _ (RUpdateRec fc cl Nothing) u = RUpdateRec fc cl (Just u)
    app fc t u = (RApp fc t u Explicit)

    doClause : List (String × Raw) → UpdateClause → M (List (String × Raw))
    doClause args (ModifyField fc nm tm) = go args
      where
        go : List (String × Raw) → M (List (String × Raw))
        go Nil = error fc "\{nm} is not a field of \{show ty}"
        go (x :: xs) = if fst x == nm
        -- need arg in here and apply tm to arg
          then pure $ (nm, app fc tm (snd x)) :: xs
          else _::_ x <$> go xs
    doClause args (AssignField fc nm tm) = go args
      where
        go : List (String × Raw) → M (List (String × Raw))
        go Nil = error fc "\{nm} is not a field of \{show ty}"
        go (x :: xs) = if fst x == nm then pure $ (nm, tm) :: xs else _::_ x <$> go xs

    collect : Raw → Tm → List (String × Raw)
    collect arg (Pi _ nm _ _ a b) = (nm, RApp fc (RVar fc $ "." ++ nm) arg Explicit) :: collect arg b
    collect _ _ = Nil

    getTele : Maybe Raw → Val → M (QName × List (String × Raw))
    getTele (Just arg) (VRef fc nm sp) = do
      top <- getTop
      let (Just (MkEntry _ _ _ (TCon _ (conname :: Nil)) _)) = lookup nm top
        | Just _ => error fc "\{show nm} is not a record"
        | _ => error fc "\{show nm} not in scope"
      let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top
        | _ => error fc "\{show conname} not a dcon"
      pure (conname, collect arg ty)
    getTele Nothing (VPi _ _ _ _ a b) = do
      a <- forceType ctx.env a
      getTele (Just $ RVar fc "$ru") a
    getTele Nothing v = error fc "Expected a pi type, got \{show v}"
    getTele (Just tm) v = error (getFC tm) "Expected a record type, got \{show v}"

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

check ctx tm ty = do
  ty' <- forceType ctx.env ty
  case (tm, ty') of
    (RUpdateRec fc clauses arg, ty) => updateRec ctx fc clauses arg ty
    (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
    (RIf fc a b c, ty) =>
      -- REVIEW maybe stuff Bool in here?
      let tm' = RCase fc a Nothing (MkAlt (RVar (getFC b) "True") (Just b) :: MkAlt (RVar (getFC c) "False") (Just c)  :: Nil) in
      check ctx tm' ty
    (RDo fc stmts, ty) => do
      body <- undo stmts
      check ctx body ty
    (RCase fc rsc mty alts, ty) => do
      (sc, scty) <- case mty of
        Nothing => infer ctx rsc
        Just ty => do
          scty <- check ctx ty (VU emptyFC)
          vscty <- eval ctx.env scty
          sc <- check ctx rsc vscty
          pure (sc, vscty)
      scty <- forceMeta scty
      debug $ \ _ => "SCTM \{rpprint (names ctx) sc}"
      debug $ \ _ => "SCTY \{show scty}"

      let scnm = fresh "sc"
      top <- getTop
      clauses <- for alts $ \case
        (MkAlt pat rawRHS) => do
          pat' <- mkPat (pat, Explicit)
          pure $ MkClause (getFC pat) ((PC scnm pat' scty) :: 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 fc (BI _ nm icit quant) tm), ty) => do
              pty <- prvalCtx ty
              -- TODO I'm hitting this with an unsolved meta
              error fc "Expected \{pty}, got a function"

    (RLet fc nm ty v sc, rty) => do
      ty' <- check ctx ty (VU emptyFC)
      vty <- eval ctx.env ty'
      v' <- check ctx v vty
      vv <- eval ctx.env 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 $ \ _ => "elab.insert: 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
      debug $ \ _ => "elab.insert: 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 "elab.insert: 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 tm@(RUpdateRec fc _ _) = error fc "I can't infer record updates"

infer ctx (RVar fc nm) = go 0 ctx.types
  where
    go : Int -> List (String × Val)  -> M (Tm × Val)
    go i Nil = do
      top <- getTop
      case lookupRaw nm top of
        Just (MkEntry _ name ty def _) => do
          debug $ \ _ => "lookup \{show name} as \{show def}"
          vty <- eval Nil ty
          pure (Ref fc name, vty)
        -- Can we soften this without introducing a meta for the type
        -- it might be additional errors, but also could lead to narrowing of possible names...
        -- especially when we hit this for .foo
        Nothing => throwError $ ENotInScope fc nm
    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 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} at \{show $ getFC tty}"
        a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env
        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 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 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 ty'
  v' <- check ctx v vty
  vv <- eval ctx.env v'
  let ctx' = define ctx nm vv vty
  (sc',scty) <- infer ctx' sc
  pure (Let fc nm v' sc', scty)

infer ctx (RLam _ (BI fc nm icit quant) tm) = do
  a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env
  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 ty
  tm <- freshMeta ctx fc vty Normal
  pure (tm, vty)

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