{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}

{-|

  This module defines the NuElim typeclass, which allows eliminations
  of (multi-) bindings. The high-level idea is that, when a fresh name
  is created with 'nu', the fresh name can also be substituted for the
  bound name in a binding. See the documentation for 'nuWithElim1' and
  'nuWithElimMulti' for details.
-}

module Data.Binding.Hobbits.NuElim (
  mbApply, mbMapAndSwap, mbRearrange,
  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1,
  NuElim(..), mkNuElimData, NuElimList(..), NuElim1(..),
  NuElimProof()
) where

--import Data.Data
import Data.Binding.Hobbits.Internal
--import Data.Binding.Hobbits.Context
import Data.Binding.Hobbits.Mb
import Data.Type.List
import Data.Type.List.Map
import Language.Haskell.TH hiding (Name)
import qualified Language.Haskell.TH as TH
--import Unsafe.Coerce (unsafeCoerce)
import Control.Monad.State
import Control.Monad.Identity

-- "proofs" that type a is an allowed type for nu-elimination; i.e.,
-- that the multi-binding of an Mb ctx a can be eliminated by nuWithElim
data NuElimProof a where
    NuElimName :: NuElimProof (Name a)
    NuElimMb :: NuElimProof a -> NuElimProof (Mb ctx a)
    NuElimFun :: NuElimProof a -> NuElimProof b -> NuElimProof (a -> b)
    NuElimData :: NuElimDataProof a -> NuElimProof a

data NuElimDataProof a =
    NuElimDataProof (forall ctx. MapC Name ctx -> MapC Name ctx -> a -> a)


-- map the names in one MapC to the corresponding ones in another
mapNamesPf :: NuElimProof a -> MapC Name ctx -> MapC Name ctx -> a -> a
mapNamesPf NuElimName Nil Nil n = n
mapNamesPf NuElimName (names :> m) (names' :> m') n =
    case cmpName m n of
      Just Refl -> m'
      Nothing -> mapNamesPf NuElimName names names' n
mapNamesPf NuElimName _ _ _ = error "Should not be possible! (in mapNamesPf)"
mapNamesPf (NuElimMb nuElim) names1 names2 (MkMb ns b) =
    undefined
{- FIXME: something like this...
    let names2' = fresh_names ns in
    MkMb names2' $ mapNamesPf (names1 |++> ns) (names2 |++> names2') b
-}
mapNamesPf (NuElimFun nuElimIn nuElimOut) names names' f =
    (mapNamesPf nuElimOut names names') . f . (mapNamesPf nuElimIn names' names)
mapNamesPf (NuElimData (NuElimDataProof mapFun)) names names' x =
    mapFun names names' x


-- just like mapNamesPf, except use the NuElim class
mapNames :: NuElim a => MapC Name ctx -> MapC Name ctx -> a -> a
mapNames = mapNamesPf nuElimProof


{-|
  Instances of the @NuElim a@ class allow the type @a@ to be used with
  'nuWithElimMulti' and 'nuWithElim1'. The structure of this class is
  mostly hidden from the user; see 'mkNuElimData' to see how to create
  instances of the @NuElim@ class.
-}
class NuElim a where
    nuElimProof :: NuElimProof a

instance NuElim (Name a) where
    nuElimProof = NuElimName

instance (NuElim a, NuElim b) => NuElim (a -> b) where
    nuElimProof = NuElimFun nuElimProof nuElimProof

{-
instance NuElim a => NuElim (Mb Nil a) where
    nuElimProof = NuElimMbNil nuElimProof

instance NuElim (Mb ctx a) => NuElim (Mb (ctx :> c) a) where
    nuElimProof = NuElimMbCons nuElimProof
-}

instance NuElim a => NuElim (Mb ctx a) where
    nuElimProof = NuElimMb nuElimProof

instance NuElim Int where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))

instance NuElim Char where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))

instance (NuElim a, NuElim b) => NuElim (a,b) where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))

instance (NuElim a, NuElim b, NuElim c) => NuElim (a,b,c) where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))

instance (NuElim a, NuElim b, NuElim c, NuElim d) => NuElim (a,b,c,d) where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))

instance (NuElim a, NuElim b) => NuElim (Either a b) where
    nuElimProof = NuElimData
                  (NuElimDataProof
                   $ (\c1 c2 x -> case x of
                                    Left l -> Left (mapNames c1 c2 l)
                                    Right r -> Right (mapNames c1 c2 r)))

instance NuElim a => NuElim [a] where
    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> map (mapNames c1 c2)))


{-
type family NuElimListProof args
type instance NuElimListProof Nil = ()
type instance NuElimListProof (args :> arg) = (NuElimListProof args, NuElimProof arg)

-- the NuElimList class, for saying that NuElim holds for a context of types
class NuElimList args where
    nuElimListProof :: NuElimListProof args

instance NuElimList Nil where
    nuElimListProof = ()

instance (NuElimList args, NuElim a) => NuElimList (args :> a) where
    nuElimListProof = (nuElimListProof, nuElimProof)
-}

data NuElimObj a = NuElim a => NuElimObj ()

-- the NuElimList class, for saying that NuElim holds for a context of types
class NuElimList args where
    nuElimListProof :: MapC NuElimObj args

instance NuElimList Nil where
    nuElimListProof = Nil

instance (NuElimList args, NuElim a) => NuElimList (args :> a) where
    nuElimListProof = nuElimListProof :> NuElimObj ()


class NuElim1 f where
    nuElimProof1 :: NuElim a => NuElimObj (f a)

-- README: deriving NuElim from NuElim1 leads to overlapping instances
-- for, e.g., Name a
{-
instance (NuElim1 f, NuElim a) => NuElim (f a) where
    nuElimProof = nuElimProof1 nuElimProof
-}

instance (NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx) where
    nuElimProof = NuElimData $ NuElimDataProof $ helper nuElimListProof where
        helper :: NuElim1 f =>
                  MapC NuElimObj args -> MapC Name ctx1 -> MapC Name ctx1 ->
                  MapC f args -> MapC f args
        helper Nil c1 c2 Nil = Nil
        helper (proofs :> NuElimObj ()) c1 c2 (elems :> (elem :: f a)) =
            case nuElimProof1 :: NuElimObj (f a) of
              NuElimObj () ->
                  (helper proofs c1 c2 elems) :>
                  mapNames c1 c2 elem

-- filter out names from a MapC Name
{-
data FilterRes where
    FilterRes :: (MapC Name ctx, MapC Name ctx) -> FilterRes

filterName :: Name a -> MapC Name ctx -> MapC Name ctx -> FilterRes
filterName n Nil Nil = Nil
filterName 

filterNames :: [Int] -> MapC Name ctx -> MapC Name ctx -> FilterRes
filterNames Nil names1 names2 = FilterRes names1 names2
Nil Nil = FilterRes Nil
filterNames (names1 :> n1)
-}

{-|
  Applies a function in a multi-binding to an argument in a
  multi-binding that binds the same number and types of names.
-}
mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
mbApply (MkMb names f) (MkMb names' a) =
    let names'' = fresh_names names in -- FIXME HERE
    MkMb names $ (mapNames names names'' f) (mapNames names' names'' a) where
        fresh_names :: MapC Name ctx -> MapC Name ctx
        fresh_names Nil = Nil
        fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)

mbMapAndSwap :: NuElim a => (Mb ctx1 a -> b) -> Mb ctx1 (Mb ctx2 a) -> Mb ctx2 b
mbMapAndSwap = undefined
{-
mbMapAndSwap (MkMb names f) (MkMb names' a) =
    MkMb names $ f $ mapNames names' names a
-}

{-|
  Take a multi-binding inside another multi-binding and move the
  outer binding inside the inner one.
-}
mbRearrange :: NuElim a => Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
mbRearrange = mbMapAndSwap id



-- FIXME: add more examples!!
{-|
  The expression @nuWithElimMulti args f@ takes a sequence @args@ of
  zero or more multi-bindings, each of type @Mb ctx ai@ for the same
  type context @ctx@ of bound names, and a function @f@ and does the
  following:

  * Creates a multi-binding that binds names @n1,...,nn@, one name for
    each type in @ctx@;

  * Substitutes the names @n1,...,nn@ for the names bound by each
    argument in the @args@ sequence, yielding the bodies of the @args@
    (using the new name @n@); and then

  * Passes the sequence @n1,...,nn@ along with the result of
    substituting into @args@ to the function @f@, which then returns
    the value for the newly created binding.

  Note that the types in @args@ must each have a @NuElim@ instance;
  this is represented with the @NuElimList@ type class.

  Here are some examples:

> commuteFun :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
> commuteFun f a =
>     nuWithElimMulti ('mbToProxy' f) ('Nil' :> f :> a)
>                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
-}
nuMultiWithElim :: (NuElimList args, NuElim b) =>
                   MapC f ctx -> MapC (Mb ctx) args ->
                   (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
nuMultiWithElim nameProxies args f =
    mbMultiApply (nuMulti nameProxies
                  (\names -> (mapCToAddArrows args (f names)))) args nuElimListProof where
        mapCToAddArrows :: MapC f args -> (MapC Identity args -> b) ->
                           AddArrows args b
        mapCToAddArrows Nil f = f Nil
        mapCToAddArrows (args :> _) f = mapCToAddArrows args (\args' x -> f (args' :> Identity x))
        mbMultiApply :: NuElim b => Mb ctx (AddArrows args b) ->
                        MapC (Mb ctx) args -> MapC NuElimObj args -> Mb ctx b
        mbMultiApply mbF Nil Nil = mbF
        mbMultiApply mbF (args :> arg) (proofs :> NuElimObj ()) =
            mbApply (mbMultiApply mbF args proofs) arg


type family AddArrows ctx a
type instance AddArrows Nil a = a
type instance AddArrows (ctx :> b) a = AddArrows ctx (b -> a)

-- README: old implementation
{-
nuMultiWithElim nameProxies args f =
    nuMulti nameProxies $ \names -> f names (mapArgs nuElimListProof args names)
    where
      mapArgs :: MapC NuElimProof args -> MapC (Mb ctx) args ->
                 MapC Name ctx -> MapC Identity args
      mapArgs Nil Nil _ = Nil
      mapArgs (proofs :> proof) (args :> arg) names =
          mapArgs proofs args names :>
                      (Identity $ mapNamesSubst proof names arg)
      mapArgs _ _ _ = error "Should not be possible! (in mapArgs)"

      mapNamesSubst :: NuElimProof arg -> MapC Name ctx -> Mb ctx arg -> arg
      mapNamesSubst proof names (MkMb namesOld arg) =
          mapNamesPf proof namesOld names arg
-}

{-|
  Similar to 'nuMultiWithElim' but binds only one name.
-}
nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args ->
              (Name a -> MapC Identity args -> b) -> Binding a b
nuWithElim args f =
    nuMultiWithElim (Nil :> Proxy) args (\(Nil :> n) -> f n)


{-|
  Similar to 'nuMultiWithElim' but takes only one argument
-}
nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg ->
                    (MapC Name ctx -> arg -> b) -> Mb ctx b
nuMultiWithElim1 nameProxies arg f =
    nuMultiWithElim nameProxies (Nil :> arg)
                    (\names (Nil :> Identity arg) -> f names arg)


{-|
  Similar to 'nuMultiWithElim' but takes only one argument that binds
  a single name.
-}
nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg ->
               (Name a -> arg -> b) -> Binding a b
nuWithElim1 (MkMb namesOld arg) f =
    nu $ \n -> f n (mapNames namesOld (Nil :> n) arg)
{-
nuWithElim1 (MkMb _ arg) f =
    error "Internal error in nuWithElim1"
-}


-- now we define some TH to create NuElimDataProofs

natsFrom i = i : natsFrom (i+1)

fst3 :: (a,b,c) -> a
fst3 (x,_,_) = x

snd3 :: (a,b,c) -> b
snd3 (_,y,_) = y

thd3 :: (a,b,c) -> c
thd3 (_,_,z) = z


type Names = (TH.Name, TH.Name, TH.Name, TH.Name)

mapNamesType a = [t| forall ctx. MapC Name ctx -> MapC Name ctx -> $a -> $a |]

{-|
  Template Haskell function for creating NuElim instances for (G)ADTs.
  Typical usage is to include the following line in the source file for
  (G)ADT @T@ (here assumed to have two type arguments):

> $(mkNuElimData [t| forall a b . T a b |])

  The 'mkNuElimData' call here will create an instance declaration for
  @'NuElim' (T a b)@. It is also possible to include a context in the
  forall type; for example, if we define the 'ID' data type as follows:

> data ID a = ID a

  then we can create a 'NuElim' instance for it like this:

> $( mkNuElimData [t| NuElim a => ID a |])

  Note that, when a context is included, the Haskell parser will add
  the @forall a@ for you.
-}
mkNuElimData :: Q Type -> Q [Dec]
mkNuElimData tQ =
    do t <- tQ
       (cxt, cType, tName, constrs, tyvars) <- getNuElimInfoTop t
       fName <- newName "f"
       x1Name <- newName "x1"
       x2Name <- newName "x2"
       clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs
       mapNamesT <- mapNamesType (return cType)
       return [InstanceD
               cxt (AppT (ConT ''NuElim) cType)
               [ValD (VarP 'nuElimProof)
                (NormalB
                 $ AppE (ConE 'NuElimData)
                   $ AppE (ConE 'NuElimDataProof)
                         $ LetE [SigD fName
                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,
                                 FunD fName clauses]
                               (VarE fName)) []]]

       {-
       return (LetE
               [SigD fName
                     (ForallT tyvars reqCxt
                     $ foldl AppT ArrowT
                           [foldl AppT (ConT conName)
                                      (map tyVarToType tyvars)]),
                FunD fname clauses]
               (VarE fname))
        -}
    where
      -- extract the name from a TyVarBndr
      tyBndrToName (PlainTV n) = n
      tyBndrToName (KindedTV n _) = n

      -- fail for getNuElimInfo
      getNuElimInfoFail t extraMsg =
          fail ("mkNuElimData: " ++ show t
                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)

      -- get info for conName (top-level call)
      getNuElimInfoTop t = getNuElimInfo [] [] t t

      -- get info for conName
      getNuElimInfo ctx tyvars topT (ConT tName) =
          do info <- reify tName
             case info of
               TyConI (DataD _ _ tyvarsReq constrs _) ->
                   success tyvarsReq constrs
               TyConI (NewtypeD _ _ tyvarsReq constr _) ->
                   success tyvarsReq [constr]
               _ -> getNuElimInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
          where
            success tyvarsReq constrs =
                let tyvarsRet = if tyvars == [] && ctx == []
                                then map tyBndrToName tyvarsReq
                                else tyvars in
                return (ctx,
                        foldl AppT (ConT tName) (map VarT tyvars),
                        tName, constrs, tyvarsRet)

      getNuElimInfo ctx tyvars topT (AppT f (VarT argName)) =
          if elem argName tyvars then
              getNuElimInfoFail topT ""
          else
              getNuElimInfo ctx (argName:tyvars) topT f

      getNuElimInfo ctx tyvars topT (ForallT _ ctx' t) =
          getNuElimInfo (ctx ++ ctx') tyvars topT t

      getNuElimInfo ctx tyvars topT t = getNuElimInfoFail topT ""

      -- get the name from a data type
      getTCtor t = getTCtorHelper t t []
      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)
      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =
          getTCtorHelper t1 topT (tyvars ++ [var])
      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
      getTCtorHelper _ _ _ = Nothing

      -- get a list of Clauses, one for each constructor in constrs
      getClauses :: Names -> [Con] -> Q [Clause]
      getClauses names constrs = mapM (getClause names) constrs

      getClause :: Names -> Con -> Q Clause
      getClause names (NormalC cName cTypes) =
          getClauseHelper names (map snd cTypes)
                          (natsFrom 0)
                          (\l -> ConP cName (map (VarP . fst3) l))
                          (\l -> foldl AppE (ConE cName) (map fst3 l))

      getClause names (RecC cName cVarTypes) =
          getClauseHelper names (map thd3 cVarTypes)
                         (map fst3 cVarTypes)
                         (\l -> RecP cName
                                (map (\(var,_,field) -> (field, VarP var)) l))
                         (\l -> RecConE cName
                                (map (\(exp,_,field) -> (field, exp)) l))

      getClause names (InfixC cType1 cName cType2) =
          undefined -- FIXME

      getClause names (ForallC _ _ con) =  getClause names con

      getClauseHelper :: Names -> [Type] -> [a] ->
                         ([(TH.Name,Type,a)] -> Pat) ->
                         ([(Exp,Type,a)] -> Exp) ->
                         Q Clause
      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =
          do varNames <- mapM (newName . ("x" ++) . show . fst)
                         $ zip (natsFrom 0) cTypes
             let varsTypesData = zip3 varNames cTypes cData
             let expsTypesData = map (mkExpTypeData names) varsTypesData
             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]
                        (NormalB $ eFun expsTypesData) []

      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)
      mkExpTypeData (tName, fName, x1Name, x2Name)
                    (varName, getTCtor -> Just (t, tName', _), cData)
          | tName == tName' =
              -- the type of the arg is the same as the (G)ADT we are
              -- recursing over; apply the recursive function
              (foldl AppE (VarE fName)
                         [(VarE x1Name), (VarE x2Name), (VarE varName)],
               t, cData)
      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =
          -- the type of the arg is not the same as the (G)ADT; call mapNames
          (foldl AppE (VarE 'mapNames)
                     [(VarE x1Name), (VarE x2Name), (VarE varName)],
           t, cData)

-- FIXME: old stuff below

type CxtStateQ a = StateT Cxt Q a

-- create a NuElimDataProof for a (G)ADT
mkNuElimDataProofOld :: Q TH.Name -> Q Exp
mkNuElimDataProofOld conNameQ =
    do conName <- conNameQ
       (cxt, name, tyvars, constrs) <- getNuElimInfo conName
       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []
       fname <- newName "f"
       return (LetE
               [SigD fname
                     (ForallT tyvars reqCxt
                     $ foldl AppT ArrowT
                           [foldl AppT (ConT conName)
                                      (map tyVarToType tyvars)]),
                FunD fname clauses]
               (VarE fname))
    where
      -- convert a TyVar to a Name
      tyVarToType (PlainTV n) = VarT n
      tyVarToType (KindedTV n _) = VarT n

      -- get info for conName
      getNuElimInfo conName =
          reify conName >>= \info ->
              case info of
                TyConI (DataD cxt name tyvars constrs _) ->
                    return (cxt, name, tyvars, constrs)
                _ -> fail ("mkNuElimDataProof: " ++ show conName
                           ++ " is not a (G)ADT")
      {-
      -- report failure
      getNuElimInfoFail t =
          fail ("mkNuElimDataProof: " ++ show t
                ++ " is not a fully applied (G)ADT")

      getNuElimInfo (ConT conName) topT =
          reify conName >>= \info ->
              case info of
                TyConI (DataD cxt name tyvars constrs _) ->
                    return (cxt, name, tyvars, constrs)
                _ -> getNuElimInfoFail topT
      getNuElimInfo (AppT t _) topT = getNuElimInfo t topT
      getNuElimInfo (SigT t _) topT = getNuElimInfo t topT
      getNuElimInfo _ topT = getNuElimInfoFail topT
       -}

      -- get a list of Clauses, one for each constructor in constrs
      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]
      getClauses cxt name tyvars constrs =
          mapM (getClause cxt name tyvars []) constrs

      getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->
                   CxtStateQ Clause
      getClause cxt name tyvars locTyvars (NormalC cName cTypes) =
          getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
                          (natsFrom 0)
                          (\l -> ConP cName (map (VarP . fst3) l))
                          (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))

      getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =
          getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
                         (map fst3 cVarTypes)
                         (\l -> RecP cName
                                (map (\(var,_,field) -> (field, VarP var)) l))
                         (\l -> RecConE cName
                                (map (\(var,_,field) -> (field, VarE var)) l))

      getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =
          undefined -- FIXME

      getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =
          getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con

      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
                         [Type] -> [a] ->
                         ([(TH.Name,Type,a)] -> Pat) ->
                         ([(TH.Name,Type,a)] -> Exp) ->
                         CxtStateQ Clause
      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
                         $ zip (natsFrom 0) cTypes
             () <- ensureCxt cxt locTyvars cTypes
             let varsTypesData = zip3 varNames cTypes cData
             return $ Clause [(pFun varsTypesData)]
                        (NormalB $ eFun varsTypesData) []

      -- ensure that NuElim a holds for each type a in cTypes
      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()
      ensureCxt cxt locTyvars cTypes =
          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes

      -- FIXME: it is not possible (or, at least, not easy) to determine
      -- if NuElim a is implied from a current Cxt... so we just add
      -- everything we need to the returned Cxt, except for 
      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()
      ensureCxt1 cxt locTyvars t = undefined
      {-
      ensureCxt1 cxt locTyvars t = do
        curCxt = get
        let fullCxt = cxt ++ curCxt
        isOk <- isNuElim fullCxt 

      isNuElim 
       -}