content: {-# LANGUAGE TupleSections, NamedFieldPuns #-}
  
  module Extract where
  
  {- extract to Fomega
  
  Examples:
  ---------
  
  MiniAgda
  
    data Vec (A : Set) : Nat -> Set
    { vnil  : Vec A zero
    ; vcons : [n : Nat] -> (head : A) -> (tail : Vec A n) -> Vec A (suc n)
    } fields head, tail
  
    fun length : [A : Set] -> [n : Nat] -> Vec A n -> <n : Nat>
    { length .A .zero    (vnil A)         = zero
    ; length .A .(suc n) (vcons A n a as) = suc (length A n as)
    }
  
  Fomega
  
    data Vec (A : Set) : Set
    { vnil  : Vec A
    ; vcons : (head : A) -> (tail : Vec A) -> Vec A
    }
  
    fun head : [A : Set] -> Vec A -> A
    { head (vcons 'head 'tail) = 'head
    }
  
    fun tail : [A : Set] -> Vec A -> A
    { head (vcons 'head 'tail) = 'tail
    }
  
    fun length : [A : Set] -> Vec A -> Nat
    { length [A]  vnil             = zero
    ; length [A] (vcons [.A] a as) = suc (length [A] as)
    }
  
  
  Bidirectional extraction
  ========================
  
  Types
  
    Base ::= D As         data type
           | ?            inexpressible type
  
    A,B ::= Base | A -> B | [x:K] -> B | [] -> B  with erasure markers
    A0, B0 ::= Base | A0 -> B0 | [x:K0] -> B0     without erasure markers
  
    |.| erase erasure markers
  
  Inference mode:
  
    Term extraction:  Gamma |- t :> A  --> e    |Gamma| |- e : |A|
    Type extraction:  Gamma |- T :> K  --> A    |Gamma| |- A : |K|
    Kind extraction:  Gamma |- U :> [] --> K    |Gamma| |- K : []
  
  Checking mode:
  
    Term extraction:  Gamma |- t <: A  --> e    |Gamma| |- e : |A|
    Type extraction:  Gamma |- T <: K  --> A    |Gamma| |- A : |K|
    Kind extraction:  Gamma |- U <: [] --> K    |Gamma| |- K : []
  
  Type and kind extraction keep erasure markers!
  
  Checking abstraction:
  
    Relevant abstraction:
    Gamma, x:A |- t <: B --> e
    --------------------------------
    Gamma |- \x.t <: A -> B --> \x.e
  
    Type abstraction:
    Gamma, x:K |- t <: B --> e : B0
    ----------------------------------------
    Gamma |- \[x].t <: [x:K] -> B --> \[x].e
        also \xt
  
    Irrelevant abstraction:
    Gamma |- t : B --> e
    -------------------------------
    Gamma |- \[x].t : [] -> B --> e
        also \xt
  
    Relevant abstraction at unknown type:
    Gamma, x:? |- t : ? --> e
    --------------------------
    Gamma |- \x.t : ? --> \x.e
  
    Irrelevant abstraction at unknown type:
    Gamma |- t : ? --> e
    -------------------------
    Gamma |- \[x].t : ? --> e
  
  Checking by inference:
  
    Gamma |- t :> A --> e    e : |A| <: |B| --> e'
    ----------------------------------------------
    Gamma |- t <: B --> e' : B0
  
  Casting:
  
    ------------------ A0 does not contain ?
    e : A0 <: A0 --> e
  
    ----------------------- A0 != B0 or one does contain ?
    e : A0 <: B0 --> cast e
  
  Inferring variable:
  
    ----------------------------
    Gamma |- x :> Gamma(x) --> x
  
  Inferring application:
  
    Relevant application:
    Gamma |- t :> A -> B --> f     Gamma |- u <: A --> e
    ----------------------------------------------------
    Gamma |- t u :> B --> f e
  
    Type application:
    Gamma |- t :> [x:K] -> B --> f   Gamma |- u <: K --> A
    ------------------------------------------------------
    Gamma |- t [u] :> : B[A/x] --> f [A]
        also  t u
  
    Irrelevant application:
    Gamma |- t :> [] -> B --> f
    ---------------------------
    Gamma |- t [u] :> B --> f
        also  t u
  
    Relevant application at unknown type:
    Gamma |- t :> ? --> f     Gamma |- u <: ? --> e
    -----------------------------------------------
    Gamma |- t u :> ? --> f e
  
    Irrelevant application at unknown type:
    Gamma |- t :> ? --> f
    -------------------------
    Gamma |- t [u] :> ? --> f
  
  
  
  -}
  
  import Prelude hiding (pi, null)
  
  #if !MIN_VERSION_base(4,8,0)
  import Control.Applicative ((<$>), (<*>))
  #endif
  import Control.Monad.Except (runExceptT)
  import Control.Monad.Reader (runReaderT)
  import Control.Monad.State  (runStateT)
  
  -- import Data.Char
  import qualified Data.Traversable as Traversable
  import qualified Data.Maybe as Maybe
  
  import Text.PrettyPrint
  
  import Polarity as Pol
  import Abstract
  import Value
  import Eval
  import TCM
  import TraceError
  import Util
  
  traceExtrM :: Monad m => String -> m ()
  traceExtrM s = return ()
  
  runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
  runExtract sig k = runExceptT (runReaderT (runStateT k (initWithSig sig)) emptyContext)
  
  -- extraction
  
  type FExpr        = Expr
  type FDeclaration = Declaration
  type FClause      = Clause
  type FPattern     = Pattern
  type FConstructor = Constructor
  type FTypeSig     = TypeSig
  type FFun         = Fun
  type FTelescope   = Telescope
  
  type FTVal        = TVal
  
  extractDecls :: [EDeclaration] -> TypeCheck [FDeclaration]
  extractDecls ds = concat <$> mapM extractDecl ds
  
  extractDecl :: EDeclaration -> TypeCheck [FDeclaration]
  extractDecl d =
    case d of
      MutualDecl _ ds -> extractDecls ds -- TODO!
      OverrideDecl{} -> throwErrorMsg $ "extractDecls internal error: overrides impossible"
      MutualFunDecl _ co funs -> extractFuns co funs
      FunDecl co fun -> extractFun co fun
      LetDecl evl x tel (Just t) e | null tel -> extractLet evl x t e
      PatternDecl{}    -> return []
      DataDecl n _ co _ tel ty cs fields -> extractDataDecl n co tel ty cs
  
  extractFuns :: Co -> [Fun] -> TypeCheck [FDeclaration]
  extractFuns co funs = do
    funs <- concat <$> mapM extractFunTypeSig funs
    concat <$> mapM (extractFun co) funs
  
  extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
  extractFun co (Fun (TypeSig n t) n' ar cls) = do
    tv <- whnf' t
    cls <- concat <$> mapM (extractClause n tv) cls
    return [ FunDecl co $ Fun (TypeSig n t) n' ar cls
           -- , LetDecl False (TypeSig n' t) (Var n)  -- no longer needed, since n and n' print the same
           ]
  
  {- OLD
  extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
  extractFun co (TypeSig n t, (ar, cls)) = extractIfTerm n $ do
    tv0 <- whnf' t
    t <- extractType tv0
    setExtrTyp n t
    let n' = mkExtName n
    setExtrTyp n' t
    tv <- whnf' t
    cls <- concat <$> mapM (extractClause n tv) cls
    return [ FunDecl co (TypeSig n t, (ar, cls))
           , LetDecl False (TypeSig n' t) (Var n)
           ]
  -}
  {-
  extractFunTypeSigs :: [Fun] -> TypeCheck [Fun]
  extractFunTypeSigs = mapM extractFunTypeSig
  -}
  
  -- only extract type sigs
  extractFunTypeSig :: Fun -> TypeCheck [Fun]
  extractFunTypeSig (Fun ts@(TypeSig n t) n' ar cls) = extractIfTerm n $ do
    ts@(TypeSig n t) <- extractTypeSig ts
    setExtrTyp n' t
    return [Fun ts n' ar cls]
  
  extractLet :: Bool -> Name -> Type -> Expr -> TypeCheck [FDeclaration]
  extractLet evl n t e = extractIfTerm n $ do
    TypeSig n t <- extractTypeSig (TypeSig n t)
    e <- extractCheck e =<< whnf' t
    return [LetDecl evl n emptyTel (Just t) e]
  
  extractTypeSig :: TypeSig -> TypeCheck FTypeSig
  extractTypeSig (TypeSig n t) = do
    t <- extractType =<< whnf' t
    setExtrTyp n t
    return $ TypeSig n t
  
  extractIfTerm :: Name -> TypeCheck [a] -> TypeCheck [a]
  extractIfTerm n cont = do
    k <- symbolKind <$> lookupSymb n
    if k == NoKind || lowerKind k == SortC Tm then cont else return []
  
  extractDataDecl :: Name -> Co -> Telescope -> Type -> [Constructor] -> TypeCheck [FDeclaration]
  extractDataDecl n co tel ty cs = do
    -- k    <- extrTyp <$> lookupSymb n
    tel' <- extractKindTel tel
    Just core <- addBinds tel $ extractKind =<< whnf' ty
    -- (_, core) = typeToTele' (length tel') k
    cs   <- mapM (extractConstructor tel) cs
    return [DataDecl n NotSized co [] tel' core cs []]
  
  extractConstructor :: Telescope -> Constructor -> TypeCheck FConstructor
  extractConstructor tel0 (Constructor n pars t) = do
  {- fails for HEq
    -- 2012-01-22: remove irrelevant parameters
    let tel = filter (\ (TBind _ dom) -> not $ erased $ decor dom)  tel0
  -}
    let tel = tel0
    -- compute full extracted constructor type and add to the signature
    t' <- extractType =<< whnf emptyEnv (teleToTypeErase tel t)
    setExtrTypQ n t'
    let (tel',core) = typeToTele' (size tel) t'
    return $ Constructor n pars core
    -- compute type minus telescope
    -- TypeSig n <$> (extractType =<< whnf' t)
  
  extractClause :: Name -> FTVal -> Clause -> TypeCheck [FClause]
  extractClause f tv (Clause _ pl Nothing) = return [] -- discard absurd clauses
  extractClause f tv cl@(Clause vtel pl (Just rhs)) = do
    traceM ("extracting clause " ++ render (prettyClause f cl)
            ++ "\n at type " ++ show tv)
  {-
    tel <- introPatterns pl tv0 $ \ _ _ -> do
             vtel <- getContextTele
             extractTeleVal vtel
    addBinds tel $
  -}
    introPatVars pl $
      extractPatterns tv pl $ \ pl tv -> do
        rhs <- extractCheck rhs tv
        return [Clause vtel pl (Just rhs)] -- TODO: return FTelescope (type!)
  
  -- the pattern variables are already in context
  extractPatterns :: FTVal -> [Pattern] ->
                     ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
  extractPatterns tv [] cont = cont [] tv
  extractPatterns tv (p:ps) cont =
    extractPattern tv p $ \ pl tv ->
      extractPatterns tv ps $ \ ps tv ->
        cont (pl ++ ps) tv
  
  extractPattern :: FTVal -> Pattern ->
                    ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
  extractPattern tv p cont = do
    traceM ("extracting pattern " ++ render (pretty p) ++ " at type " ++ show tv)
    fv <- funView tv
    case fv of
      EraseArg tv -> cont [] tv  -- skip erased patterns
  
      Forall x dom fv -> do
        xv <- whnf' (patternToExpr p) -- pattern variables are already in scope
        bv <- app fv xv -- TODO!
        case p of
          ErasedP (VarP y) -> setTypeOfName y dom $ cont [] bv
          _ -> cont [] bv
  {-
      Forall x ki env t -> new x ki $ \ xv ->
        cont [] =<< whnf (update env x xv) t -- TODO!
  -}
      Arrow av bv -> extractPattern' av p (flip cont bv)
  
  extractPattern' :: FTVal -> Pattern ->
                    ([FPattern] -> TypeCheck a) -> TypeCheck a
  extractPattern' av p cont =
        case p of
          VarP y -> setTypeOfName y (defaultDomain av) $
            cont [VarP y]
          PairP p1 p2 -> do
            view <- prodView av
            -- hack to avoid IMPOSSIBLE
            let (av1, av2) = case view of
                               Prod av1 av2 -> (av1, av2)
                               _ -> (av, av) -- HACK
            extractPattern' av1 p1 $ \ ps1 -> do
              extractPattern' av2 p2 $ \ ps2 ->
                 let ps [] ps2    = ps2
                     ps ps1 []    = ps1
                     ps [p1] [p2] = [PairP p1 p2]
                 in  cont $ ps ps1 ps2
  
  {-
            case view of
              Prod av1 av2 ->
                extractPattern' av1 p1 $ \ [p1] -> do
                  extractPattern' av2 p2 $ \ [p2] -> cont [PairP p1 p2]
              _ -> throwErrorMsg $ "extractPattern': IMPOSSIBLE: pattern " ++
                            show p ++ " : " ++ show av
  -}
          ConP pi n ps -> do
  --          tv <- whnf' =<< extrTyp <$> lookupSymb n
            tv <- extrConType n av
            extractPatterns tv ps $ \ ps _ ->
              cont [ConP pi n ps]
          _ -> cont []
  
  extrConType :: QName -> FTVal -> TypeCheck FTVal
  extrConType c av = do
    ConSig { conPars, extrTyp, dataPars } <- lookupSymbQ c
    traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)
    tv <- whnf' extrTyp
    numPars <- maybe (return dataPars) (const $ throwErrorMsg $ "NYI: extrConType for pattern parameters") conPars
    case numPars of
     0 -> return tv
     _ -> do
      case av of
        VApp (VDef (DefId DatK d)) vs -> do
          DataSig { positivity } <- lookupSymbQ d
          traceExtrM ("extrConType " ++ show c ++ "; data type has positivity = " ++ show positivity)
          let pars 0 pols vs = []
              pars n (pol:pols) vs | erased pol = VIrr : pars (n-1) pols vs
              pars n (pol:pols) (v:vs) = v : pars (n-1) pols vs
              pars n pols vs = error $ "pars " ++ show n ++ show pols ++ show vs
          piApps tv $ pars numPars positivity $ vs ++ repeat VIrr
  {-
          let (pars, inds) = splitAt numPars vs
          piApps tv pars
  -}
        _ -> piApps tv $ replicate numPars VIrr
  --      _ -> throwErrorMsg $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av
  
  -- extracting a term from a term -------------------------------------
  
  extractInfer :: Expr -> TypeCheck (FExpr, FTVal)
  extractInfer e = do
    case e of
  
      Var x -> (Var x,) . typ . domain <$> lookupName1 x
  
      App f e0 -> do
        let (er, e) = isErasedExpr e0
        (f, tv) <- extractInfer f
        fv <- funView tv
        case fv of
          EraseArg bv -> return (f,bv)
          Forall x dom fv -> do
            e <- extractTypeAt e (typ dom)
            bv <- app fv =<< whnf' e
            return $ (App f (erasedExpr e), bv)
          Arrow av bv -> return (if er then f else App f e, bv)
          NotFun -> return (if er then f else castExpr f `App` e, VIrr)
  
      Def f -> (Def f,) <$> do (whnf' . extrTyp) =<< lookupSymbQ (idName f)
  
      Pair{} -> throwErrorMsg $ "extractInfer: IMPOSSIBLE: pair " ++ show e
      -- other expressions are erased or types
  
      _ -> return (Irr, VIrr)
  
  extractCheck :: Expr -> FTVal -> TypeCheck (FExpr)
  extractCheck e tv = do
    case e of
      Lam dec y e -> do
        fv <- funView tv
        case fv of
          EraseArg bv        -> extractCheck e bv -- discard lambda
          Forall x dom fv    ->
            Lam (decor dom) y <$> do
              newWithGen y dom $ \ i xv ->
                extractCheck e =<< app fv (VGen i) -- no eta-expansion
          Arrow av bv        ->
            if erased dec then extractCheck e bv
             else Lam dec y <$> do
               new' y (defaultDomain av) $
                 extractCheck e bv
          NotFun            -> castExpr <$>
            if erased dec then extractCheck e VIrr
             else Lam dec y <$> do
               new' y (defaultDomain VIrr) $
                 extractCheck e VIrr
  
      LLet (TBind x dom0) tel e1 e2 | null tel -> do
        let dom = fmap Maybe.fromJust dom0
        if erased (decor dom) then extractCheck e2 tv else do -- discard let
         vdom <- Traversable.mapM whnf' dom         -- MiniAgda type val
         dom  <- Traversable.mapM extractType vdom  -- Fomega type
         vdom <- Traversable.mapM whnf' dom         -- Fomega type val
         e1  <- extractCheck e1 (typ vdom)
         LLet (TBind x (fmap Just dom)) emptyTel e1 <$> do
           new' x vdom $ extractCheck e2 tv
  
      Pair e1 e2 -> do
        view <- prodView tv
        let (av1,av2) = case view of
                          Prod av1 av2 -> (av1, av2)
                          _ -> (tv,tv) -- HACK!!
        Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
  {-
        case view of
          Prod av1 av2 -> Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
          _ -> throwErrorMsg $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv
  -}
  
      -- TODO: case
  
      _ -> fallback
    where
      fallback = do
        (e,tv') <- extractInfer e
        insertCast e tv tv'
  
  insertCast :: FExpr -> FTVal -> FTVal -> TypeCheck FExpr
  insertCast e tv1 tv2 = loop tv1 tv2 where
    loop tv1 tv2 =
      case (tv1,tv2) of
        (VIrr,_) -> return $ castExpr e
        (_,VIrr) -> return $ castExpr e
        _  -> return e -- TODO!
  
  funView :: FTVal -> TypeCheck FunView
  funView tv =
    case tv of
      -- erasure mark
      VQuant Pi x dom fv | erased (decor dom) && typ dom == VIrr ->
        EraseArg <$> app fv VIrr
      -- forall
      VQuant Pi x dom fv | erased (decor dom) ->
        return $ Forall x dom fv
      -- function type
      VQuant Pi x dom fv ->
        Arrow (typ dom) <$> app fv VIrr
      -- any other type can be a function type, but this needs casts!
      _ -> return NotFun -- $ Arrow VIrr VIrr
  
  data FunView
    = Arrow    FTVal FTVal            -- A -> B
    | Forall   Name Domain FTVal      -- forall X:K. A
    | EraseArg FTVal                  -- [] -> B
    | NotFun                          -- ()
  
  prodView :: FTVal -> TypeCheck ProdView
  prodView tv =
    case tv of
      VQuant Sigma x dom fv -> Prod (typ dom) <$> app fv VIrr
      _                     -> return $ NotProd
  
  data ProdView
    = Prod FTVal FTVal -- A * B
    | NotProd
  
  -- extracting a kind from a value ------------------------------------
  
  type FKind = Expr -- FKind ::= Set | FKind -> FKind | [Irr] -> FKind
  
  star :: FKind
  star = Sort $ Set Zero
  
  extractSet :: Sort Val -> Maybe FKind
  extractSet s =
    case s of
      SortC _ -> Nothing
      Set _   -> Just $ star
      CoSet _ -> Just $ star
  
  -- keep irrelevant entries
  extractKindTel :: Telescope -> TypeCheck FTelescope
  extractKindTel (Telescope tel) = Telescope <$> loop tel where
    loop [] = return []
    loop (TBind x dom : tel) = do
      dom  <- Traversable.mapM whnf' dom
      dom' <- extractKindDom dom
      if erased (decor dom') then
        newIrr x $
          (TBind x dom' :) <$> loop tel
       else newTyVar x (typ dom') $ \ i -> do
          x <- nameOfGen i
          (TBind x dom' :) <$> loop tel
  
  {-
  -- keep irrelevant entries
  extractKindTel :: Telescope -> TypeCheck FTelescope
  extractKindTel tel = do
    tv     <- whnf' (teleToType tel star)
    Just k <- extractKind tv
    let (tel, s) = typeToTele k
    return tel
    -- throw away erasure marks
    -- return $ filter (\ tb -> not $ erased $ decor $ boundDom tb) tel
  -}
  
  extractKindDom :: Domain -> TypeCheck (Dom FKind)
  extractKindDom dom =
    maybe (defaultIrrDom Irr) defaultDomain <$>
      if erased (decor dom) then return Nothing
       else extractKind (typ dom)
  
  extractKind :: TVal -> TypeCheck (Maybe FKind)
  extractKind tv =
    case tv of
      VSort s -> return $ extractSet s
      VMeasured mu vb -> extractKind vb
      VGuard beta vb -> extractKind vb
      VQuant Pi x dom fv -> new' x dom $ do
         bv  <- app fv VIrr
         mk' <- extractKind bv
         case mk' of
           Nothing -> return Nothing
           Just k' -> do
             dom' <- extractKindDom dom
             let x = fresh ""
             return $ Just $ pi (TBind x dom') k'
      _ -> return Nothing
  
  -- extracting a type constructor from a value ------------------------
  
  type FType = Expr
  {- FType ::= Irr                 -- not expressible in Fomega
             | D FTypes            -- data type
             | X FTypes            -- type variable
             | FType -> FType      -- function type
             | [X:FKind] -> FType  -- polymorphic type
             | [Irr] -> FType      -- erasure marker
   -}
  
  -- tyVarName i = fresh $ "a" ++ show i
  
  newTyVar :: Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
  newTyVar x k cont = newWithGen x (defaultDomain (VClos emptyEnv k)) $
    \ i _ -> cont i                  -- store kinds unevaluated
  
  addFKindTel :: FTelescope -> TypeCheck a -> TypeCheck a
  addFKindTel (Telescope tel) = loop tel where
    loop []                  cont = cont
    loop (TBind x dom : tel) cont = newTyVar x (typ dom) $ \ _ ->
      loop tel cont
  
  extractTeleVal :: TeleVal -> TypeCheck FTelescope
  extractTeleVal = Telescope <.> loop where
    loop []          = return []
    loop (tb : vtel) = do
      tb <- Traversable.mapM extractType tb
      addBind tb $ do
        (tb :) <$> loop vtel
  
  extractType :: TVal -> TypeCheck FType
  extractType = extractTypeAt star
  
  extractTypeAt :: FKind -> TVal -> TypeCheck FType
  extractTypeAt k tv = do
    case (tv,k) of
  
      (VMeasured mu vb, _) -> extractTypeAt k vb
      (VGuard beta vb, _) -> extractTypeAt k vb
  
      -- relevant function space / sigma type --> non-dependent
      (VQuant pisig x dom fv, _) | not (erased (decor dom)) -> do
        a <- extractType (typ dom)
        -- new' x dom $ do
        bv <- app fv VIrr
        b  <- extractType bv
        let x = fresh ""
        return $ piSig pisig (TBind x (defaultDomain a)) b
  
      -- irrelevant function space --> forall or erasure marker
      (VQuant Pi x dom fv, _) | erased (decor dom) -> do
        mk <- extractKind (typ dom)
        case mk of
          Nothing -> do -- new' x dom $ do
            bv <- app fv VIrr
            b  <- extractType bv
            let x = fresh ""
            return $ pi (TBind x (defaultIrrDom Irr)) b
          Just k' -> do
            newTyVar x k' $ \ i -> do
              bv <- app fv $ VGen i
              b  <- extractType bv
              x  <- nameOfGen i
              return $ pi (TBind x (defaultIrrDom k')) b
  
      (VApp (VDef (DefId DatK n)) vs, _) -> do
        k  <- extrTyp <$> lookupSymbQ n  -- get kind of dname from signature
        as <- extractTypes k vs  -- turn vs into types as at kind k
        return $ foldl App (Def (DefId DatK n)) as
  
      (VGen i,_) -> do
  --      VClos _ k <- (typ . fromOne . domain) <$> lookupGen i  -- get kind of var from cxt
        Var <$> nameOfGen i
        -- return $ Var (tyVarName i)
  
      (VApp (VGen i) vs,_) -> do
        VClos _ k <- (typ . fromOne . domain) <$> lookupGen i  -- get kind of var from cxt
        as <- extractTypes k vs  -- turn vs into types as at kind k
        x <- nameOfGen i
        return $ foldl App (Var x) as
  
      (VLam x env e, Quant Pi (TBind _ dom) k) | erased (decor dom) -> do
        tv <- whnf (update env x VIrr) e
        extractTypeAt k tv
  
      (VLam x env e, Quant Pi (TBind _ dom) k) -> newTyVar x (typ dom) $ \ i -> do
        tv <- whnf (update env x (VGen i)) e
        x  <- nameOfGen i
        Lam defaultDec x <$> extractTypeAt k tv
  
      (VLam{},_) -> error $ "panic! extractTypeAt " ++ show (tv,k)
  
      (VSing _ tv,_) -> extractTypeAt k tv
  
      (VUp v _,_)    -> extractTypeAt k v
  
      _ -> return Irr
  
  extractTypes :: FKind -> [TVal] -> TypeCheck [FType]
  extractTypes k vs =
    case (k,vs) of
      (_, []) -> return []
      (Quant Pi (TBind _ dom) k, v:vs) | erased (decor dom) -> extractTypes k vs
      (Quant Pi (TBind _ dom) k, v:vs) -> do
        v  <- whnfClos v
        a  <- extractTypeAt (typ dom) v
        as <- extractTypes k vs
        return $ a : as
      _ -> error $ "panic! extractTypes  " ++ show k ++ "  " ++ show vs
  
  -- auxiliary functions -----------------------------------------------
  
  {- this is setExtrTyp
  addFTypeSig :: Name -> FType -> TypeCheck ()
  addFTypeSig n t = modifySig n (\ item -> item { extrTyp = t })
  -}
  