module Agda.TypeChecking.Generalize
  ( generalizeType
  , generalizeType'
  , generalizeTelescope ) where

import Prelude hiding (null)

import Control.Arrow (first)
import Control.Monad
import Control.Monad.Except

import qualified Data.IntSet as IntSet
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS
import Data.List (partition, sortBy)
import Data.Monoid
import Data.Function (on)

import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (LensInScope(..))
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Monad (bindVariable, outsideLocalVars)
import Agda.Syntax.Scope.Base (BindingSource(..))
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

import Agda.Benchmarking (Phase(Typing, Generalize))
import Agda.Utils.Benchmark
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List (downFrom, hasElem)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple

-- | Generalize a telescope over a set of generalizable variables.
generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
generalizeTelescope :: forall a.
Map QName Name
-> (forall a. (Telescope -> TCM a) -> TCM a)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars forall a. (Telescope -> TCM a) -> TCM a
typecheckAction [Maybe Name] -> Telescope -> TCM a
ret | forall k a. Map k a -> Bool
Map.null Map QName Name
vars = forall a. (Telescope -> TCM a) -> TCM a
typecheckAction ([Maybe Name] -> Telescope -> TCM a
ret [])
generalizeTelescope Map QName Name
vars forall a. (Telescope -> TCM a) -> TCM a
typecheckAction [Maybe Name] -> Telescope -> TCM a
ret = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Typing, Phase
Generalize] forall a b. (a -> b) -> a -> b
$ forall a. (Type -> TCM a) -> TCM a
withGenRecVar forall a b. (a -> b) -> a -> b
$ \ Type
genRecMeta -> do
  let s :: Set QName
s = forall k a. Map k a -> Set k
Map.keysSet Map QName Name
vars
  (([Name]
cxtNames, Telescope
tel, [(Name, (Term, Dom Type))]
letbinds), Map MetaId QName
namedMetas, LocalMetaStores
allmetas) <-
    forall a.
Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
createMetasAndTypeCheck Set QName
s forall a b. (a -> b) -> a -> b
$ forall a. (Telescope -> TCM a) -> TCM a
typecheckAction forall a b. (a -> b) -> a -> b
$ \ Telescope
tel -> do
      Context
cxt <- forall a. Int -> [a] -> [a]
take (forall a. Sized a => a -> Int
size Telescope
tel) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      [(Name, (Term, Dom Type))]
lbs <- forall (tcm :: * -> *).
MonadTCM tcm =>
tcm [(Name, (Term, Dom Type))]
getLetBindings -- This gives let-bindings valid in the current context
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
cxt, Telescope
tel, [(Name, (Term, Dom Type))]
lbs)
  -- Translate the QName to the corresponding bound variable
  (Telescope
genTel, [Maybe QName]
genTelNames, Substitution
sub) <- forall name.
Type
-> Map MetaId name
-> LocalMetaStores
-> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization Type
genRecMeta Map MetaId QName
namedMetas LocalMetaStores
allmetas

  let boundVar :: QName -> Name
boundVar QName
q = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
q Map QName Name
vars
      genTelVars :: [Maybe Name]
genTelVars = (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) QName -> Name
boundVar [Maybe QName]
genTelNames

  Telescope
tel' <- forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Telescope
tel

  -- This is not so nice. When changing the context from Γ (r : R) to Γ Δ we need to do this at the
  -- level of contexts (as a Context -> Context function), so we repeat the name logic here. Take
  -- care to preserve the name of named generalized variables.
  let setName :: c -> f (b, d) -> f (c, d)
setName c
name f (b, d)
d = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a b. a -> b -> a
const c
name) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b, d)
d
      cxtEntry :: (Maybe Name, Dom' t (b, d)) -> m (Dom' t (Name, d))
cxtEntry (Maybe Name
mname, Dom' t (b, d)
d) = do
          Name
name <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. LensInScope a => a -> a
setNotInScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ b
s) forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
mname
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *} {c} {b} {d}.
Functor f =>
c -> f (b, d) -> f (c, d)
setName Name
name Dom' t (b, d)
d
        where s :: b
s  = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t (b, d)
d
      dropCxt :: Impossible -> m a -> m a
dropCxt Impossible
err = forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext (forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
1) (forall a. Int -> [a] -> [a]
drop Int
1)
  Context
genTelCxt <- forall {m :: * -> *} {a}.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *} {b} {t} {d}.
(FreshName b, MonadFresh NameId m) =>
(Maybe Name, Dom' t (b, d)) -> m (Dom' t (Name, d))
cxtEntry forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Name]
genTelVars forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
genTel

  -- For the explicit module telescope we get the names from the typecheck
  -- action.
  let newTelCxt :: Context
newTelCxt = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {f :: * -> *} {c} {b} {d}.
Functor f =>
c -> f (b, d) -> f (c, d)
setName [Name]
cxtNames forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel'

  -- We are in context Γ (r : R) and should call the continuation in context Γ Δ Θρ passing it Δ Θρ
  -- We have
  --   Γ (r : R) ⊢ Θ            Θ = tel
  --   Γ ⊢ Δ                    Δ = genTel
  --   Γ Δ ⊢ ρ : Γ (r : R)      ρ = sub
  --   Γ ⊢ Δ Θρ                 Θρ = tel'
  -- And we shouldn't forget about the let-bindings (#3470)
  --   Γ (r : R) Θ ⊢ letbinds
  --   Γ Δ Θρ      ⊢ letbinds' = letbinds(lift |Θ| ρ)
  [(Name, (Term, Dom Type))]
letbinds' <- forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
tel) Substitution
sub) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [(Name, (Term, Dom Type))]
letbinds
  let addLet :: (Name, (Term, Dom Type)) -> m a -> m a
addLet (Name
x, (Term
v, Dom Type
dom)) = forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
x Term
v Dom Type
dom

  forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
sub ((Context
genTelCxt forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
1) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext (forall a. Int -> Substitution' a
raiseS (forall a. Sized a => a -> Int
size Telescope
tel')) (Context
newTelCxt forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {m :: * -> *} {a}.
MonadAddContext m =>
(Name, (Term, Dom Type)) -> m a -> m a
addLet ([Maybe Name] -> Telescope -> TCM a
ret [Maybe Name]
genTelVars forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Telescope -> t -> t
abstract Telescope
genTel Telescope
tel') [(Name, (Term, Dom Type))]
letbinds'


-- | Generalize a type over a set of (used) generalizable variables.
generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s TCM Type
typecheckAction = do
  ([Maybe QName]
ns, Type
t, ()
_) <- forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s forall a b. (a -> b) -> a -> b
$ (,()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
typecheckAction
  forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe QName]
ns, Type
t)

-- | Allow returning additional information from the type checking action.
generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' :: forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s TCM (Type, a)
typecheckAction = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [Phase
Typing, Phase
Generalize] forall a b. (a -> b) -> a -> b
$ forall a. (Type -> TCM a) -> TCM a
withGenRecVar forall a b. (a -> b) -> a -> b
$ \ Type
genRecMeta -> do

  ((Type
t, a
userdata), Map MetaId QName
namedMetas, LocalMetaStores
allmetas) <- forall a.
Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
createMetasAndTypeCheck Set QName
s TCM (Type, a)
typecheckAction
  (Telescope
genTel, [Maybe QName]
genTelNames, Substitution
sub) <- forall name.
Type
-> Map MetaId name
-> LocalMetaStores
-> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization Type
genRecMeta Map MetaId QName
namedMetas LocalMetaStores
allmetas

  Type
t' <- forall t. Abstract t => Telescope -> t -> t
abstract Telescope
genTel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"generalized"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Int
1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t') ]

  forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe QName]
genTelNames, Type
t', a
userdata)

-- | Create metas for the generalizable variables and run the type check action.
createMetasAndTypeCheck ::
  Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
createMetasAndTypeCheck :: forall a.
Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
createMetasAndTypeCheck Set QName
s TCM a
typecheckAction = do
  ((Map MetaId QName
namedMetas, a
x), LocalMetaStores
allmetas) <- forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy forall a b. (a -> b) -> a -> b
$ do
    (Map MetaId QName
metamap, Map QName GeneralizedValue
genvals) <- Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues Set QName
s
    a
x <- forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map QName GeneralizedValue) TCEnv
eGeneralizedVars (forall a b. a -> b -> a
const Map QName GeneralizedValue
genvals) TCM a
typecheckAction
    forall (m :: * -> *) a. Monad m => a -> m a
return (Map MetaId QName
metamap, a
x)
  forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, Map MetaId QName
namedMetas, LocalMetaStores
allmetas)

-- | Add a placeholder variable that will be substituted with a record value packing up all the
--   generalized variables.
withGenRecVar :: (Type -> TCM a) -> TCM a
withGenRecVar :: forall a. (Type -> TCM a) -> TCM a
withGenRecVar Type -> TCM a
ret = do
  -- Create a meta type (in Set₀) for the telescope record. It won't
  -- necessarily fit in Set₀, but since it's only used locally the sort
  -- shouldn't matter. Another option would be to put it in Setω, which is a
  -- bit more honest, but this leads to performance problems (see #3306).
  Type
genRecMeta <- Sort -> TCM Type
newTypeMeta (Integer -> Sort
mkType Integer
0)
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. a -> Dom a
defaultDom (String
"genTel" :: String, Type
genRecMeta)) forall a b. (a -> b) -> a -> b
$ Type -> TCM a
ret Type
genRecMeta

-- | Compute the generalized telescope from metas created when checking the *thing* (type or telescope) to be
--   generalized. Called in the context extended with the telescope record variable (whose type is
--   the first argument). Returns the telescope of generalized variables and a substitution from
--   this telescope to the current context.
computeGeneralization
  :: Type
       -- ^ The metavariable to be instantiated with record type containing
       --   as fields the variables generalized in the *thing*.
  -> Map MetaId name
       -- ^ Metas created from an occurrence of a @variable@. (The original free variables.)
       --   E.g. if you have
       --   @
       --     variable  l : Level; A : Set l
       --     postulate f : A → A
       --   @
       --   then @A@ would be in this @Map@, but not @l@.
  -> LocalMetaStores
       -- ^ The metas created when type-checking the *thing*.
  -> TCM (Telescope, [Maybe name], Substitution)
       -- ^ The telescope together with binder name (left-to-right order),
       --   and substitution from this telescope to the current context.
computeGeneralization :: forall name.
Type
-> Map MetaId name
-> LocalMetaStores
-> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization Type
genRecMeta Map MetaId name
nameMap LocalMetaStores
allmetas = forall a. TCM a -> TCM a
postponeInstanceConstraints forall a b. (a -> b) -> a -> b
$ do

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"computing generalization for type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
genRecMeta

  -- Pair metas with their metaInfo
  let mvs :: [(MetaId, MetaVariable)]
mvs = forall k a. Map k a -> [(k, a)]
MapS.assocs (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
allmetas) forall a. [a] -> [a] -> [a]
++
            forall k a. Map k a -> [(k, a)]
MapS.assocs (LocalMetaStores -> LocalMetaStore
solvedMetas LocalMetaStores
allmetas)

  -- Issue 4727: filter out metavariables that were created before the
  -- current checkpoint, since they are too old to be generalized.
  -- TODO: make metasCreatedBy smarter so it doesn't see pruned
  -- versions of old metas as new metas.
  CheckpointId
cp <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  let isFreshMeta :: MonadReduce m => (MetaId, MetaVariable) -> m Bool
      isFreshMeta :: forall (m :: * -> *).
MonadReduce m =>
(MetaId, MetaVariable) -> m Bool
isFreshMeta (MetaId
x,MetaVariable
mv) = forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ -> forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe Substitution)
checkpointSubstitution' CheckpointId
cp
  [(MetaId, MetaVariable)]
mvs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall (m :: * -> *).
MonadReduce m =>
(MetaId, MetaVariable) -> m Bool
isFreshMeta [(MetaId, MetaVariable)]
mvs
  [ProblemConstraint]
cs <- forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stAwakeConstraints
             forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stSleepingConstraints

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"current constraints:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemConstraint]
cs)

  Set MetaId
constrainedMetas <- forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Constraint -> TCMT IO (Set MetaId)
constraintMetas forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Closure a -> a
clValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"constrainedMetas     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set MetaId
constrainedMetas)

  let isConstrained :: MetaId -> Bool
isConstrained MetaId
x = forall a. Ord a => a -> Set a -> Bool
Set.member MetaId
x Set MetaId
constrainedMetas
      -- Note: Always generalize named metas even if they are constrained. We
      -- freeze them so they won't be instantiated by the constraint, and we do
      -- want the nice error from checking the constraint after generalization.
      -- See #3276.
      isGeneralizable :: (MetaId, MetaVariable) -> Bool
isGeneralizable (MetaId
x, MetaVariable
mv) = forall k a. Ord k => k -> Map k a -> Bool
Map.member MetaId
x Map MetaId name
nameMap Bool -> Bool -> Bool
||
                                Bool -> Bool
not (MetaId -> Bool
isConstrained MetaId
x) Bool -> Bool -> Bool
&& DoGeneralize
NoGeneralize forall a. Eq a => a -> a -> Bool
/= forall e. Arg e -> e
unArg (MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv))
      isSort :: (a, MetaVariable) -> Bool
isSort = MetaVariable -> Bool
isSortMeta_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
      isOpen :: (a, MetaVariable) -> Bool
isOpen = MetaInstantiation -> Bool
isOpenMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd

  -- Split the generalizable metas in open and closed
  let ([(MetaId, MetaVariable)]
generalizable, [(MetaId, MetaVariable)]
nongeneralizable)         = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (MetaId, MetaVariable) -> Bool
isGeneralizable [(MetaId, MetaVariable)]
mvs
      ([(MetaId, MetaVariable)]
generalizableOpen', [(MetaId, MetaVariable)]
generalizableClosed) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall {a}. (a, MetaVariable) -> Bool
isOpen [(MetaId, MetaVariable)]
generalizable
      ([(MetaId, MetaVariable)]
openSortMetas, [(MetaId, MetaVariable)]
generalizableOpen)        = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall {a}. (a, MetaVariable) -> Bool
isSort [(MetaId, MetaVariable)]
generalizableOpen'
      nongeneralizableOpen :: [(MetaId, MetaVariable)]
nongeneralizableOpen                      = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (a, MetaVariable) -> Bool
isOpen [(MetaId, MetaVariable)]
nongeneralizable

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"generalizable        = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(MetaId, MetaVariable)]
generalizable)
    , TCMT IO Doc
"generalizableOpen    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(MetaId, MetaVariable)]
generalizableOpen)
    , TCMT IO Doc
"openSortMetas        = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(MetaId, MetaVariable)]
openSortMetas)
    ]

  -- Issue 3301: We can't generalize over sorts
  forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(MetaId, MetaVariable)]
openSortMetas forall a b. (a -> b) -> a -> b
$ \ [(MetaId, MetaVariable)]
ms ->
    forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ [MetaId] -> Warning
CantGeneralizeOverSorts forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(MetaId, MetaVariable)]
ms

  -- Any meta in the solution of a generalizable meta should be generalized over (if possible).
  CheckpointId
cp <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  let canGeneralize :: MetaId -> TCMT IO Bool
canGeneralize MetaId
x | MetaId -> Bool
isConstrained MetaId
x = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      canGeneralize MetaId
x = do
          MetaVariable
mv   <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
          Maybe Substitution
msub <- forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ ->
                    forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe Substitution)
checkpointSubstitution' CheckpointId
cp
          let sameContext :: Bool
sameContext =
                -- We can only generalize if the metavariable takes the context variables of the
                -- current context as arguments. This happens either when the context of the meta
                -- is the same as the current context and there is no pruning, or the meta context
                -- is a weakening but the extra variables have been pruned.
                -- It would be possible to generalize also in the case when some context variables
                -- (other than genTel) have been pruned, but it's hard to construct an example
                -- where this actually happens.
                case (Maybe Substitution
msub, MetaVariable -> Permutation
mvPermutation MetaVariable
mv) of
                  (Just Substitution
IdS, Perm Int
m [Int]
xs)        -> [Int]
xs forall a. Eq a => a -> a -> Bool
== [Int
0 .. Int
m forall a. Num a => a -> a -> a
- Int
1]
                  (Just (Wk Int
n Substitution
IdS), Perm Int
m [Int]
xs) -> [Int]
xs forall a. Eq a => a -> a -> Bool
== [Int
0 .. Int
m forall a. Num a => a -> a -> a
- Int
n forall a. Num a => a -> a -> a
- Int
1]
                  (Maybe Substitution, Permutation)
_                            -> Bool
False
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
sameContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
20 forall a b. (a -> b) -> a -> b
$ do
            Type
ty <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
x
            let Perm Int
m [Int]
xs = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
            forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Don't know how to generalize over"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty
              , forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in context"
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
              , forall (m :: * -> *). Applicative m => String -> m Doc
text String
"permutation:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show (Int
m, [Int]
xs))
              , forall (m :: * -> *). Applicative m => String -> m Doc
text String
"subst:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe Substitution
msub ]
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sameContext
  Set MetaId
inherited <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(MetaId, MetaVariable)]
generalizableClosed forall a b. (a -> b) -> a -> b
$ \ (MetaId
x, MetaVariable
mv) ->
    case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
      InstV Instantiation
inst -> do
        String
parentName <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m String
getMetaNameSuggestion MetaId
x
        [MetaId]
metas <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
canGeneralize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                 forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                 forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Instantiation -> Term
instBody Instantiation
inst)
        let suggestNames :: Integer -> [MetaId] -> TCMT IO ()
suggestNames Integer
i [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
            suggestNames Integer
i (MetaId
m : [MetaId]
ms) = do
              -- #4291: Override existing meta name suggestion. If we solved the parent with a new
              --        meta use the parent name for that, otherwise suffix with a number.
              let suf :: String
suf | forall a. Null a => a -> Bool
null [MetaId]
ms Bool -> Bool -> Bool
&& Integer
i forall a. Eq a => a -> a -> Bool
== Integer
1,
                        MetaV{} <- Instantiation -> Term
instBody Instantiation
inst = String
""
                      | Bool
otherwise                = String
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i
              forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
setMetaNameSuggestion MetaId
m (String
parentName forall a. [a] -> [a] -> [a]
++ String
suf)
              Integer -> [MetaId] -> TCMT IO ()
suggestNames (Integer
i forall a. Num a => a -> a -> a
+ Integer
1) [MetaId]
ms
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [MetaId]
metas) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat [TCMT IO Doc
"Inherited metas from ", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x, TCMT IO Doc
":"] forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [MetaId]
metas)
                                    -- Don't suggest names for explicitly named generalizable metas
        forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Integer -> [MetaId] -> TCMT IO ()
suggestNames Integer
1 (forall a. (a -> Bool) -> [a] -> [a]
filter (forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map MetaId name
nameMap) [MetaId]
metas)
      MetaInstantiation
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

  let ([MetaId]
alsoGeneralize, [MetaId]
reallyDontGeneralize) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
inherited) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(MetaId, MetaVariable)]
nongeneralizableOpen
      generalizeOver :: [MetaId]
generalizeOver   = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(MetaId, MetaVariable)]
generalizableOpen forall a. [a] -> [a] -> [a]
++ [MetaId]
alsoGeneralize
      shouldGeneralize :: MetaId -> Bool
shouldGeneralize = ([MetaId]
generalizeOver forall a. Ord a => [a] -> a -> Bool
`hasElem`)

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"alsoGeneralize       = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [MetaId]
alsoGeneralize)
    , TCMT IO Doc
"reallyDontGeneralize = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [MetaId]
reallyDontGeneralize)
    ]

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"we're generalizing over" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [MetaId]
generalizeOver)

  -- Sort metas in dependency order. Include open metas that we are not
  -- generalizing over, since they will need to be pruned appropriately (see
  -- Issue 3672).
  [MetaId]
allSortedMetas <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
GeneralizeCyclicDependency) forall a b. (a -> b) -> a -> b
$
    [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas ([MetaId]
generalizeOver forall a. [a] -> [a] -> [a]
++ [MetaId]
reallyDontGeneralize forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(MetaId, MetaVariable)]
openSortMetas)
  let sortedMetas :: [MetaId]
sortedMetas = forall a. (a -> Bool) -> [a] -> [a]
filter MetaId -> Bool
shouldGeneralize [MetaId]
allSortedMetas

  let dropCxt :: Impossible -> m a -> m a
dropCxt Impossible
err = forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext (forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
1) (forall a. Int -> [a] -> [a]
drop Int
1)

  -- Create the pre-record type (we don't yet know the types of the fields)
  (QName
genRecName, ConHead
genRecCon, [QName]
genRecFields) <- forall {m :: * -> *} {a}.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
      Type -> [MetaId] -> TCMT IO (QName, ConHead, [QName])
createGenRecordType Type
genRecMeta [MetaId]
sortedMetas

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"created genRecordType"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"genRecName   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
genRecName
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"genRecCon    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
genRecCon
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"genRecFields = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
genRecFields)
    ]

  -- Solve the generalizable metas. Each generalizable meta is solved by projecting the
  -- corresponding field from the genTel record.
  Telescope
cxtTel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let solve :: MetaId -> QName -> TCMT IO ()
solve MetaId
m QName
field = do
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"solving generalized meta" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
field])
        -- m should not be instantiated, but if we don't check constraints
        -- properly it could be (#3666 and #3667). Fail hard instead of
        -- generating bogus types.
        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
m) forall a. HasCallStack => a
__IMPOSSIBLE__
        forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg String] -> Term -> m ()
assignTerm' MetaId
m (forall a. TelToArgs a => a -> [Arg String]
telToArgs Telescope
cxtTel) forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
field]
  forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ MetaId -> QName -> TCMT IO ()
solve [MetaId]
sortedMetas [QName]
genRecFields

  -- Record the named variables in the telescope
  let telNames :: [Maybe name]
telNames = forall a b. (a -> b) -> [a] -> [b]
map (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map MetaId name
nameMap) [MetaId]
sortedMetas

  -- Build the telescope of generalized metas
  [(Arg String, Type)]
teleTypes <- do
    Args
args <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
sortedMetas forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
      MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      let info :: ArgInfo
info =
            forall a. LensHiding a => a -> a
hideOrKeepInstance forall a b. (a -> b) -> a -> b
$
            forall a. LensArgInfo a => a -> ArgInfo
getArgInfo forall a b. (a -> b) -> a -> b
$ MetaInfo -> Arg DoGeneralize
miGeneralizable forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
          HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } = MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
          perm :: Permutation
perm = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
      Type
t' <- forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
t forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
perm) Args
args
      forall (m :: * -> *) a. Monad m => a -> m a
return [(forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall a b. (a -> b) -> a -> b
$ MetaInfo -> String
miNameSuggestion forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv, Type
t')]
  let genTel :: Telescope
genTel = ConHead -> [(Arg String, Type)] -> Telescope
buildGeneralizeTel ConHead
genRecCon [(Arg String, Type)]
teleTypes

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"genTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
genTel ]

  -- Now we need to prune the unsolved metas to make sure they respect the new
  -- dependencies (#3672). Also update interaction points to point to pruned metas.
  let inscope :: (InteractionId, InteractionPoint) -> Maybe (MetaId, InteractionId)
inscope (InteractionId
ii, InteractionPoint{ipMeta :: InteractionPoint -> Maybe MetaId
ipMeta = Just MetaId
x})
        | forall k a. Ord k => k -> Map k a -> Bool
MapS.member MetaId
x (LocalMetaStores -> LocalMetaStore
openMetas LocalMetaStores
allmetas) Bool -> Bool -> Bool
||
          forall k a. Ord k => k -> Map k a -> Bool
MapS.member MetaId
x (LocalMetaStores -> LocalMetaStore
solvedMetas LocalMetaStores
allmetas) =
          forall a. a -> Maybe a
Just (MetaId
x, InteractionId
ii)
      inscope (InteractionId, InteractionPoint)
_ = forall a. Maybe a
Nothing
  Map MetaId InteractionId
ips <- forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe (MetaId, InteractionId)
inscope forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
BiMap.toDistinctAscendingLists forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BiMap InteractionId InteractionPoint) TCState
stInteractionPoints
  QName
-> ConHead
-> Telescope
-> [QName]
-> Map MetaId InteractionId
-> (MetaId -> Bool)
-> [MetaId]
-> TCMT IO ()
pruneUnsolvedMetas QName
genRecName ConHead
genRecCon Telescope
genTel [QName]
genRecFields Map MetaId InteractionId
ips MetaId -> Bool
shouldGeneralize [MetaId]
allSortedMetas

  -- Fill in the missing details of the telescope record.
  forall {m :: * -> *} {a}.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ QName -> ConHead -> [QName] -> Type -> Telescope -> TCMT IO ()
fillInGenRecordDetails QName
genRecName ConHead
genRecCon [QName]
genRecFields Type
genRecMeta Telescope
genTel

  -- Now abstract over the telescope. We need to apply the substitution that subsitutes a record
  -- value packing up the generalized variables for the genTel variable.
  let sub :: Substitution
sub = ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub ConHead
genRecCon (forall a b. (a -> b) -> [a] -> [b]
map (forall e. Arg e -> ArgInfo
argInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Arg String, Type)]
teleTypes) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Arg String, Type)]
teleTypes)

  -- Instantiate all fresh meta-variables to get rid of
  -- __DUMMY_TERM__.
  Telescope
genTel <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
(MetaId -> ReduceM Bool) -> a -> m a
instantiateWhen Telescope
genTel forall a b. (a -> b) -> a -> b
$ \MetaId
m -> do
    Maybe (Either RemoteMetaVariable MetaVariable)
mv <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
    case Maybe (Either RemoteMetaVariable MetaVariable)
mv of
      Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Just Left{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Just (Right MetaVariable
mv) -> forall (m :: * -> *).
MonadReduce m =>
(MetaId, MetaVariable) -> m Bool
isFreshMeta (MetaId
m, MetaVariable
mv)

  forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
genTel, [Maybe name]
telNames, Substitution
sub)

-- | Prune unsolved metas (#3672). The input includes also the generalized metas and is sorted in
-- dependency order. The telescope is the generalized telescope.
pruneUnsolvedMetas :: QName -> ConHead -> Telescope -> [QName] -> Map MetaId InteractionId -> (MetaId -> Bool) -> [MetaId] -> TCM ()
pruneUnsolvedMetas :: QName
-> ConHead
-> Telescope
-> [QName]
-> Map MetaId InteractionId
-> (MetaId -> Bool)
-> [MetaId]
-> TCMT IO ()
pruneUnsolvedMetas QName
genRecName ConHead
genRecCon Telescope
genTel [QName]
genRecFields Map MetaId InteractionId
interactionPoints MetaId -> Bool
isGeneralized [MetaId]
metas
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all MetaId -> Bool
isGeneralized [MetaId]
metas = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise               = [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [] Telescope
genTel [MetaId]
metas
  where
    prune :: [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [Dom (String, Type)]
_ Telescope
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    prune [Dom (String, Type)]
cxt Telescope
tel (MetaId
x : [MetaId]
xs) | Bool -> Bool
not (MetaId -> Bool
isGeneralized MetaId
x) = do
      -- If x is a blocked term we shouldn't instantiate it.
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
x) forall a b. (a -> b) -> a -> b
$ do
        MetaId
x <- if forall a. Sized a => a -> Int
size Telescope
tel forall a. Ord a => a -> a -> Bool
> Int
0 then MetaId -> TCMT IO MetaId
prePrune MetaId
x
                             else forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x
        Telescope -> MetaId -> TCMT IO ()
pruneMeta ([Dom (String, Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Dom (String, Type)]
cxt) MetaId
x
      [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [Dom (String, Type)]
cxt Telescope
tel [MetaId]
xs
    prune [Dom (String, Type)]
cxt (ExtendTel Dom Type
a Abs Telescope
tel) (MetaId
x : [MetaId]
xs) = [Dom (String, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
x,) Dom Type
a forall a. a -> [a] -> [a]
: [Dom (String, Type)]
cxt) (forall a. Abs a -> a
unAbs Abs Telescope
tel) [MetaId]
xs
      where x :: String
x = forall a. Abs a -> String
absName Abs Telescope
tel
    prune [Dom (String, Type)]
_ Telescope
_ [MetaId]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

    sub :: Int -> Substitution
sub = ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub ConHead
genRecCon forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
genTel

    prepruneErrorRefinedContext :: MetaId -> TCM a
prepruneErrorRefinedContext = forall a. String -> MetaId -> TCM a
prepruneError forall a b. (a -> b) -> a -> b
$
      String
"Failed to generalize because some of the generalized variables depend on an " forall a. [a] -> [a] -> [a]
++
      String
"unsolved meta created in a refined context (not a simple extension of the context where " forall a. [a] -> [a] -> [a]
++
      String
"generalization happens)."

    prepruneErrorCyclicDependencies :: MetaId -> TCM a
prepruneErrorCyclicDependencies = forall a. String -> MetaId -> TCM a
prepruneError forall a b. (a -> b) -> a -> b
$
      String
"Failed to generalize due to circular dependencies between the generalized " forall a. [a] -> [a] -> [a]
++
      String
"variables and an unsolved meta."

    prepruneErrorFailedToInstantiate :: MetaId -> TCM a
prepruneErrorFailedToInstantiate = forall a. String -> MetaId -> TCM a
prepruneError forall a b. (a -> b) -> a -> b
$
      String
"Failed to generalize because the generalized variables depend on an unsolved meta " forall a. [a] -> [a] -> [a]
++
      String
"that could not be lifted outside the generalization."

    prepruneError :: String -> MetaId -> TCM a
    prepruneError :: forall a. String -> MetaId -> TCM a
prepruneError String
msg MetaId
x = do
      Range
r <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        (forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String
msg forall a. [a] -> [a] -> [a]
++ String
" The problematic unsolved meta is") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
                 (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x []) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Range
r)
        )

    -- If one of the fields depend on this meta, we have to make sure that this meta doesn't depend
    -- on any variables introduced after the genRec. See test/Fail/Issue3672b.agda for a test case.
    prePrune :: MetaId -> TCMT IO MetaId
prePrune MetaId
x = do
      CheckpointId
cp <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
      MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
      (Int
i, Maybe Type
_A) <- forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do
        Substitution
δ <- forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm Substitution
checkpointSubstitution CheckpointId
cp
        Maybe Type
_A <- case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
                IsSort{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                HasType{} -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
x
        case Substitution
δ of
          Wk Int
n Substitution
IdS -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, Maybe Type
_A)
          Substitution
IdS      -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
0, Maybe Type
_A)
          Substitution
_        -> forall {a}. MetaId -> TCM a
prepruneErrorRefinedContext MetaId
x
      if Int
i forall a. Eq a => a -> a -> Bool
== Int
0 then forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x else do
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune.pre" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"prepruning"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. Judgement a -> Type
jMetaType forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"|Δ| =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow Int
i ]

        -- We have
        --   Γ (r : GenRec)            current context
        --   Γ (r : GenRec) Δ ⊢ x : A  with |Δ| = i
        -- and we need to get rid of the dependency on Δ.

        -- We can only do this if A does not depend on Δ, so check this first.
        case IntSet -> Maybe (Int, IntSet)
IntSet.minView (forall t. Free t => t -> IntSet
allFreeVars Maybe Type
_A) of
          Just (Int
j, IntSet
_) | Int
j forall a. Ord a => a -> a -> Bool
< Int
i -> forall {a}. MetaId -> TCM a
prepruneErrorCyclicDependencies MetaId
x
          Maybe (Int, IntSet)
_                   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

        -- If it doesn't we can strenghten it to the current context (this is done by
        -- newMetaFromOld).
        --   Γ (r : GenRec) ⊢ ρ : Γ (r : GenRec) Δ
        let ρ :: Substitution
ρ  = forall a. Impossible -> Int -> Substitution' a
strengthenS HasCallStack => Impossible
impossible Int
i
            ρ' :: Substitution
ρ' = forall a. Int -> Substitution' a
raiseS Int
i

        (MetaId
y, Term
u) <- MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
newMetaFromOld MetaVariable
mv Substitution
ρ Maybe Type
_A

        let uρ' :: Term
uρ' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
ρ' Term
u

        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune.pre" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"u    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
u
          , TCMT IO Doc
"uρ⁻¹ =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
uρ' ]

        -- To solve it we enter the context of x again
        forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do
          -- v is x applied to the context variables
          Term
v <- case Maybe Type
_A of
                 Maybe Type
Nothing -> Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
                 Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
          forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
doPrune MetaId
x MetaVariable
mv Maybe Type
_A Term
v Term
uρ') forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> forall {a}. MetaId -> TCM a
prepruneErrorFailedToInstantiate MetaId
x
          MetaId -> MetaId -> TCMT IO ()
setInteractionPoint MetaId
x MetaId
y
          forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
y

    pruneMeta :: Telescope -> MetaId -> TCMT IO ()
pruneMeta Telescope
_Θ MetaId
x = do
      CheckpointId
cp <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
      MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
      -- The reason we are doing all this inside the closure of x is so that if x is an interaction
      -- meta we get the right context for the pruned interaction meta.
      forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ ->
        -- If we can't find the generalized record, it's already been pruned and we don't have to do
        -- anything.
        forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (MetaVariable -> TCM (Maybe Int)
findGenRec MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ \ Int
i -> do

        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"pruning"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"GenRecTel is var" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
i ]

        Telescope
_ΓrΔ <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
        let (Telescope
_Γ, Telescope
_Δ) = ([Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
gs, [Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
ds)
              where ([Dom (String, Type)]
gs, Dom (String, Type)
_ : [Dom (String, Type)]
ds) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Int
size Telescope
_ΓrΔ forall a. Num a => a -> a -> a
- Int
i forall a. Num a => a -> a -> a
- Int
1) (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
_ΓrΔ)

        -- Get the type of x. By doing this here we let the checkpoint machinery sort out the
        Maybe Type
_A <- case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
                IsSort{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                HasType{} -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
x

        -- We have
        --   Γ  (r : GenTel) Δ         current context
        --   Γ₀ (r : GenTel)           top context
        --   Γ₀ ⊢ Θ                    prefix of the generalized telescope currently in scope
        --   Γ (r : GenTel) Δ ⊢ x : A  the meta to prune

        -- Get the substitution from the point of generalization to the current context. This always
        -- succeeds since if the meta depends on GenTel it must have been created inside the
        -- generalization:
        --   Γ (r : GenTel) Δ ⊢ δ : Γ₀ (r : GenTel)
        Substitution
δ <- forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm Substitution
checkpointSubstitution CheckpointId
cp

        -- v is x applied to the context variables
        Term
v <- case Maybe Type
_A of
               Maybe Type
Nothing -> Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
               Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv

        -- Now ultimately we want to create the fresh meta in the context
        --   Γ Θγ Δσ where Γ    ⊢ γ : Γ₀
        --                 Γ Θγ ⊢ σ : Γ (r : GenTel)
        -- σ is the unpacking substitution (which is polymorphic in Γ)
        let σ :: Substitution
σ   = Int -> Substitution
sub (forall a. Sized a => a -> Int
size Telescope
_Θ)
            --    Γ <- Γ (r : GenTel) Δ <- Γ₀ (r : GenTel) <- Γ₀
            γ :: Substitution
γ   = forall a. Impossible -> Int -> Substitution' a
strengthenS HasCallStack => Impossible
impossible (Int
i forall a. Num a => a -> a -> a
+ Int
1) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
δ forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall a. Int -> Substitution' a
raiseS Int
1
            _Θγ :: Telescope
_Θγ = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
γ Telescope
_Θ
            _Δσ :: Telescope
_Δσ = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
σ Telescope
_Δ

        -- The substitution into the new context is simply lifting σ over Δ:
        --   Γ Θγ Δσ ⊢ lift i σ : Γ (r : GenTel) Δ
        let ρ :: Substitution
ρ  = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i Substitution
σ
            -- We also need ρ⁻¹, which is a lot easier to construct.
            ρ' :: Substitution
ρ' = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i forall a b. (a -> b) -> a -> b
$ [ Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld] | QName
fld <- forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall a. Sized a => a -> Int
size Telescope
_Θ) forall a b. (a -> b) -> a -> b
$ [QName]
genRecFields ] forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Int -> Substitution' a
raiseS Int
1

        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"Γ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Γ
          , TCMT IO Doc
"Θ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Θ
          , TCMT IO Doc
"Δ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Δ
          , TCMT IO Doc
"σ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
σ
          , TCMT IO Doc
"γ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
γ
          , TCMT IO Doc
"δ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
δ
          , TCMT IO Doc
"ρ   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
ρ
          , TCMT IO Doc
"ρ⁻¹ =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
ρ'
          , TCMT IO Doc
"Θγ  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Θγ
          , TCMT IO Doc
"Δσ  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Δσ
          , TCMT IO Doc
"_A  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe Type
_A
          ]

        -- When updating the context we also need to pick names for the variables. Get them from the
        -- current context and generate fresh ones for the generalized variables in Θ.
        (Context
newCxt, Context
rΘ) <- do
          (Context
rΔ, Dom' Term (Name, Type)
_ : Context
rΓ) <- forall a. Int -> [a] -> ([a], [a])
splitAt Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
          let setName :: Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t))
setName = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ \ (String
s, t
ty) -> (,t
ty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
          Context
rΘ <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t}. Dom' Term (String, t) -> TCMT IO (Dom' Term (Name, t))
setName forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
_Θγ
          let rΔσ :: Context
rΔσ = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Name
name Dom (String, Type)
dom -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a b. a -> b -> a
const Name
name) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom (String, Type)
dom)
                            (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
rΔ)
                            (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
_Δσ)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Context
rΔσ forall a. [a] -> [a] -> [a]
++ Context
rΘ forall a. [a] -> [a] -> [a]
++ Context
rΓ, Context
rΘ)

        -- Now we can enter the new context and create our meta variable.
        (MetaId
y, Term
u) <- forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
ρ (forall a b. a -> b -> a
const Context
newCxt) forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
localScope forall a b. (a -> b) -> a -> b
$ do

          -- First, we add the named variables to the scope, to allow
          -- them to be used in holes (#3341). These should go outside Δ (#3735).
          forall a. Int -> ScopeM a -> ScopeM a
outsideLocalVars Int
i forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {t} {b}.
Foldable t =>
t (Dom' t (Name, b)) -> TCMT IO ()
addNamedVariablesToScope Context
rΘ

          -- Now we can create the new meta
          MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
newMetaFromOld MetaVariable
mv Substitution
ρ Maybe Type
_A

        -- Finally we solve x := yρ⁻¹. The reason for solving it this way instead of xρ := y is that
        -- ρ contains dummy terms for the variables that are not in scope.
        -- If x has been instantiated by some constraint unblocked by previous pruning or
        -- generalization, use equalTerm instead of assigning to x. If this fails (see
        -- test/Fail/Issue3655b.agda for a test case), we need to give an error. This can happen if
        -- there are dependencies between generalized variables that are hidden by constraints and
        -- the dependency sorting happens to pick the wrong order. For instance, if we have
        --    α : Nat   (unsolved meta)
        --    t : F α   (named variable)
        --    n : Nat   (named variable)
        -- and a constraint F α == F n, where F does some pattern matching preventing the constraint
        -- to be solved when n is still a meta. If t appears before n in the type these will be sorted
        -- as α, t, n, but we will solve α := n before we get to the pruning here. It's good that we
        -- solve first though, because that means we can give a more informative error message than
        -- the "Cannot instantiate..." we would otherwise get.
        let uρ' :: Term
uρ' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
ρ' Term
u
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"solving"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v   forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
                         , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
uρ' forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
                         , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe Type
_A ] ]
        forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
doPrune MetaId
x MetaVariable
mv Maybe Type
_A Term
v Term
uρ') forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` MetaId -> Term -> TCErr -> TCMT IO ()
niceError MetaId
x Term
v

        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize.prune" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"solved"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v)
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"uρ⁻¹ =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
uρ') ]

        MetaId -> MetaId -> TCMT IO ()
setInteractionPoint MetaId
x MetaId
y

    findGenRec :: MetaVariable -> TCM (Maybe Int)
    findGenRec :: MetaVariable -> TCM (Maybe Int)
findGenRec MetaVariable
mv = do
      Context
cxt <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      let n :: Int
n         = forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
cxt
          notPruned :: IntSet
notPruned = [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$
                      forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP Int
n forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) forall a b. (a -> b) -> a -> b
$
                      forall a. Integral a => a -> [a]
downFrom Int
n
      case [ Int
i
           | (Int
i, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (Name
_, El Sort
_ (Def QName
q Elims
_))}) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Context
cxt
           , QName
q forall a. Eq a => a -> a -> Bool
== QName
genRecName
           , Int
i Int -> IntSet -> Bool
`IntSet.member` IntSet
notPruned
           ] of
        []    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Int
_:Int
_:[Int]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
        [Int
i]   -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Int
i)
                                                    -- Nothing if sort meta
    newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
    newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
newMetaFromOld MetaVariable
mv Substitution
ρ Maybe Type
mA = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv forall a b. (a -> b) -> a -> b
$
      case Maybe Type
mA of
        Maybe Type
Nothing -> do
          s :: Sort
s@(MetaS MetaId
y Elims
_) <- forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
          forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
y, Sort -> Term
Sort Sort
s)
        Just Type
_A -> do
          let _Aρ :: Type
_Aρ = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
ρ Type
_A
          forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> String -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck
                            (MetaInfo -> String
miNameSuggestion forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
                            (forall a. Judgement a -> Comparison
jComparison forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv) Type
_Aρ

    -- If x is a hole, update the hole to point to y instead.
    setInteractionPoint :: MetaId -> MetaId -> TCMT IO ()
setInteractionPoint MetaId
x MetaId
y =
      forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MetaId
x Map MetaId InteractionId
interactionPoints) (forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
`connectInteractionPoint` MetaId
y)

    doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCM ()
    doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCMT IO ()
doPrune MetaId
x MetaVariable
mv Maybe Type
mt Term
v Term
u =
      case Maybe Type
mt of
        Maybe Type
_ | Bool
isOpen -> CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> TCMT IO ()
assign CompareDirection
DirEq MetaId
x (Term -> Args
getArgs Term
v) Term
u forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe CompareAs
AsTypes Type -> CompareAs
AsTermsOf Maybe Type
mt
        Maybe Type
Nothing    -> forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Term -> Sort
unwrapSort Term
v) (Term -> Sort
unwrapSort Term
u)
        Just Type
t     -> forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t Term
v Term
u
      where
        isOpen :: Bool
isOpen = MetaInstantiation -> Bool
isOpenMeta forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv
        getArgs :: Term -> Args
getArgs = \case
            Sort (MetaS MetaId
_ Elims
es) -> forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
            MetaV MetaId
_ Elims
es        -> forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
            Term
_                 -> forall a. HasCallStack => a
__IMPOSSIBLE__
        unwrapSort :: Term -> Sort
unwrapSort (Sort Sort
s) = Sort
s
        unwrapSort Term
_        = forall a. HasCallStack => a
__IMPOSSIBLE__

    niceError :: MetaId -> Term -> TCErr -> TCMT IO ()
niceError MetaId
x Term
u TCErr
err = do
      Term
u <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
u
      let err' :: TCErr
err' = case TCErr
err of
                   TypeError{tcErrClosErr :: TCErr -> Closure TypeError
tcErrClosErr = Closure TypeError
cl} ->
                     -- Remove the 'when' part from the error since it's most like the same as ours.
                     TCErr
err{ tcErrClosErr :: Closure TypeError
tcErrClosErr = Closure TypeError
cl{ clEnv :: TCEnv
clEnv = (forall a. Closure a -> TCEnv
clEnv Closure TypeError
cl) { envCall :: Maybe (Closure Call)
envCall = forall a. Maybe a
Nothing } } }
                   TCErr
_ -> TCErr
err
          telList :: [Dom (String, Type)]
telList = forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
genTel
          names :: [String]
names   = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom (String, Type)]
telList
          late :: [String]
late    = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Any -> Bool
getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (Bool -> Any
Any forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
== MetaId
x))) [Dom (String, Type)]
telList
          projs :: Elim' Term -> Set String
projs (Proj ProjOrigin
_ QName
q)
            | QName
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
genRecFields = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [QName -> Maybe String
getGeneralizedFieldName QName
q]
          projs Elim' Term
_                 = forall a. Set a
Set.empty
          early :: [String]
early = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term
u forall a b. (a -> b) -> a -> b
$ \ case
                  Var Int
_ Elims
es   -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set String
projs Elims
es
                  Def QName
_ Elims
es   -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set String
projs Elims
es
                  MetaV MetaId
_ Elims
es -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set String
projs Elims
es
                  Term
_          -> forall a. Set a
Set.empty
          commas :: [String] -> String
commas []       = forall a. HasCallStack => a
__IMPOSSIBLE__
          commas [String
x]      = String
x
          commas [String
x, String
y]   = String
x forall a. [a] -> [a] -> [a]
++ String
", and " forall a. [a] -> [a] -> [a]
++ String
y
          commas (String
x : [String]
xs) = String
x forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ [String] -> String
commas [String]
xs
          cause :: String
cause = String
"There were unsolved constraints that obscured the " forall a. [a] -> [a] -> [a]
++
                  String
"dependencies between the generalized variables."
          solution :: String
solution = String
"The most reliable solution is to provide enough information to make the dependencies " forall a. [a] -> [a] -> [a]
++
                     String
"clear, but simply mentioning the variables in the right order should also work."
          order :: TCMT IO Doc
order = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Dependency analysis suggested this (likely incorrect) order:",
                        forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
fwords ([String] -> String
unwords [String]
names) ]
          guess :: String
guess = String
"After constraint solving it looks like " forall a. [a] -> [a] -> [a]
++ [String] -> String
commas [String]
late forall a. [a] -> [a] -> [a]
++ String
" actually depend" forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++
                  String
" on " forall a. [a] -> [a] -> [a]
++ [String] -> String
commas [String]
early
            where
              s :: String
s | forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
late forall a. Eq a => a -> a -> Bool
== Int
1 = String
"s"
                | Bool
otherwise        = String
""
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *). Applicative m => String -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ String
"Variable generalization failed."
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [TCMT IO Doc
"- Probable cause", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
cause]
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [TCMT IO Doc
"- Suggestion", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
solution]
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc
"- Further information"
                         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
order ] forall a. [a] -> [a] -> [a]
++
                         [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
guess | Bool -> Bool
not (forall a. Null a => a -> Bool
null [String]
late), Bool -> Bool
not (forall a. Null a => a -> Bool
null [String]
early) ] forall a. [a] -> [a] -> [a]
++
                         [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"The dependency I error is", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM TCErr
err' ] ]
        ]

    addNamedVariablesToScope :: t (Dom' t (Name, b)) -> TCMT IO ()
addNamedVariablesToScope t (Dom' t (Name, b))
cxt =
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ t (Dom' t (Name, b))
cxt forall a b. (a -> b) -> a -> b
$ \ Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (Name
x, b
_) } -> do
        -- Recognize named variables by lack of '.' (TODO: hacky!)
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.generalize.eta.scope" Int
40 forall a b. (a -> b) -> a -> b
$ String
"Adding (or not) " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
x) forall a. [a] -> [a] -> [a]
++ String
" to the scope"
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Char
'.' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
x)) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.generalize.eta.scope" Int
40 String
"  (added)"
          BindingSource -> Name -> Name -> TCMT IO ()
bindVariable BindingSource
LambdaBound (Name -> Name
nameConcrete Name
x) Name
x

-- | Create a substition from a context where the i first record fields are variables to a context
--   where you have a single variable of the record type. Packs up the field variables in a record
--   constructor and pads with __DUMMY_TERM__s for the missing fields. Important that you apply this
--   to terms that only projects the defined fields from the record variable.
--   Used with partial record values when building the telescope of generalized variables in which
--   case we have done the dependency analysis that guarantees it is safe.
unpackSub :: ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub :: ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub ConHead
con [ArgInfo]
infos Int
i = Substitution
recSub
  where
    ar :: Int
ar = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgInfo]
infos
    appl :: ArgInfo -> a -> Elim' a
appl ArgInfo
info a
v = forall a. Arg a -> Elim' a
Apply (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
v)
    recVal :: Term
recVal = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. ArgInfo -> a -> Elim' a
appl [ArgInfo]
infos forall a b. (a -> b) -> a -> b
$ [Int -> Term
var Int
j | Int
j <- [Int
i forall a. Num a => a -> a -> a
- Int
1, Int
i forall a. Num a => a -> a -> a
- Int
2..Int
0]] forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
ar forall a. Num a => a -> a -> a
- Int
i) HasCallStack => Term
__DUMMY_TERM__

    -- want: Γ Δᵢ ⊢ recSub i : Γ (r : R)
    -- have:
    -- Γ Δᵢ ⊢ recVal i :# σ : Θ (r : R),  if Γ Δᵢ ⊢ σ : Θ
    -- Γ Δᵢ ⊢ WkS i IdS : Γ
    recSub :: Substitution
recSub = Term
recVal forall a. a -> Substitution' a -> Substitution' a
:# forall a. Int -> Substitution' a -> Substitution' a
Wk Int
i forall a. Substitution' a
IdS

-- | Takes the list of types
--    A₁ []
--    A₂ [r.f₁]
--    A₃ [r.f₂, r.f₃]
--    ...
--   And builds the telescope
--    (x₁ : A₁ [ r := c _       .. _ ])
--    (x₂ : A₂ [ r := c x₁ _    .. _ ])
--    (x₃ : A₃ [ r := c x₁ x₂ _ .. _ ])
--    ...
buildGeneralizeTel :: ConHead -> [(Arg String, Type)] -> Telescope
buildGeneralizeTel :: ConHead -> [(Arg String, Type)] -> Telescope
buildGeneralizeTel ConHead
con [(Arg String, Type)]
xs = Int -> [(Arg String, Type)] -> Telescope
go Int
0 [(Arg String, Type)]
xs
  where
    infos :: [ArgInfo]
infos = forall a b. (a -> b) -> [a] -> [b]
map (forall e. Arg e -> ArgInfo
argInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Arg String, Type)]
xs
    recSub :: Int -> Substitution
recSub Int
i = ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub ConHead
con [ArgInfo]
infos Int
i
    go :: Int -> [(Arg String, Type)] -> Telescope
go Int
_ [] = forall a. Tele a
EmptyTel
    go Int
i ((Arg String
name, Type
ty) : [(Arg String, Type)]
xs) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
dom Type
ty') forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs (forall e. Arg e -> e
unArg Arg String
name) forall a b. (a -> b) -> a -> b
$ Int -> [(Arg String, Type)] -> Telescope
go (Int
i forall a. Num a => a -> a -> a
+ Int
1) [(Arg String, Type)]
xs
      where ty' :: Type
ty' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution
recSub Int
i) Type
ty
            dom :: Type -> Dom Type
dom = forall a. ArgInfo -> String -> a -> Dom a
defaultNamedArgDom (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg String
name) (forall e. Arg e -> e
unArg Arg String
name)

-- | Create metas for all used generalizable variables and their dependencies.
createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues Set QName
s = do
  [(QName, MetaId, GeneralizedValue)]
genvals <- forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' DoGeneralize TCEnv
eGeneralizeMetas (forall a b. a -> b -> a
const DoGeneralize
YesGeneralizeVar) forall a b. (a -> b) -> a -> b
$
               forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCM (QName, MetaId, GeneralizedValue)
createGenValue forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. HasRange a => a -> Range
getRange) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set QName
s
  let metaMap :: Map MetaId QName
metaMap = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ [ (MetaId
m, QName
x) | (QName
x, MetaId
m, GeneralizedValue
_) <- [(QName, MetaId, GeneralizedValue)]
genvals ]
      nameMap :: Map QName GeneralizedValue
nameMap = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ [ (QName
x, GeneralizedValue
v) | (QName
x, MetaId
_, GeneralizedValue
v) <- [(QName, MetaId, GeneralizedValue)]
genvals ]
  forall (m :: * -> *) a. Monad m => a -> m a
return (Map MetaId QName
metaMap, Map QName GeneralizedValue
nameMap)

-- | Create a generalisable meta for a generalisable variable.
createGenValue :: QName -> TCM (QName, MetaId, GeneralizedValue)
createGenValue :: QName -> TCM (QName, MetaId, GeneralizedValue)
createGenValue QName
x = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x forall a b. (a -> b) -> a -> b
$ do
  CheckpointId
cp  <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
                   -- Only prefix of generalizable arguments (for now?)
  let nGen :: Int
nGen       = case Definition -> NumGeneralizableArgs
defArgGeneralizable Definition
def of
                     NumGeneralizableArgs
NoGeneralizableArgs     -> Int
0
                     SomeGeneralizableArgs Int
n -> Int
n
      ty :: Type
ty         = Definition -> Type
defType Definition
def
      TelV Telescope
tel Type
_ = Type -> TelV Type
telView' Type
ty
      -- Generalizable variables are never explicit, so if they're given as
      -- explicit we default to hidden.
      hideExplicit :: a -> a
hideExplicit a
arg | forall a. LensHiding a => a -> Bool
visible a
arg = forall a. LensHiding a => a -> a
hide a
arg
                       | Bool
otherwise   = a
arg
      argTel :: Telescope
argTel     = [Dom (String, Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensHiding a => a -> a
hideExplicit forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
nGen forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel

  Args
args <- forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
newTelMeta Telescope
argTel
  Type
metaType <- forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
ty Args
args

  let name :: String
name     = forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)
  (MetaId
m, Term
term) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> String -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck String
name Comparison
CmpLeq Type
metaType

  -- Freeze the meta to prevent named generalizable metas from being
  -- instantiated, and set the quantity of the meta to the declared
  -- quantity of the generalisable variable.
  forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
    forall a. LensQuantity a => Quantity -> a -> a
setQuantity (forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> ArgInfo
defArgInfo Definition
def)) forall a b. (a -> b) -> a -> b
$
    MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }

  -- Set up names of arg metas
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Integer
1..] (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
args) (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
argTel)) forall a b. (a -> b) -> a -> b
$ \ case
    (Integer
i, MetaV MetaId
m Elims
_, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (String
x, Type
_)}) -> do
      let suf :: String -> String
suf String
"_" = forall a. Show a => a -> String
show Integer
i
          suf String
""  = forall a. Show a => a -> String
show Integer
i
          suf String
x   = String
x
      forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
setMetaNameSuggestion MetaId
m (String
name forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ String -> String
suf String
x)
    (Integer, Term, Dom (String, Type))
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- eta expanded

  -- Update the ArgInfos for the named meta. The argument metas are
  -- created with the correct ArgInfo.
  forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> a
hideExplicit (Definition -> ArgInfo
defArgInfo Definition
def)

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"created metas for generalized variable" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"top  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
term
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
args ]

  case Term
term of
    MetaV{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Term
_       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCMT IO Doc
"Cannot generalize over" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"of eta-expandable type") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
                                    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
metaType
  forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x, MetaId
m, GeneralizedValue{ genvalCheckpoint :: CheckpointId
genvalCheckpoint = CheckpointId
cp
                                , genvalTerm :: Term
genvalTerm       = Term
term
                                , genvalType :: Type
genvalType       = Type
metaType })

-- | Create a not-yet correct record type for the generalized telescope. It's not yet correct since
--   we haven't computed the telescope yet, and we need the record type to do it.
createGenRecordType :: Type -> [MetaId] -> TCM (QName, ConHead, [QName])
createGenRecordType :: Type -> [MetaId] -> TCMT IO (QName, ConHead, [QName])
createGenRecordType genRecMeta :: Type
genRecMeta@(El Sort
genRecSort Term
_) [MetaId]
sortedMetas = do
  ModuleName
current <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  let freshQName :: String -> TCMT IO QName
freshQName String
s = ModuleName -> Name -> QName
qualify ModuleName
current forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
s :: String)
      mkFieldName :: MetaId -> TCMT IO QName
mkFieldName  = String -> TCMT IO QName
freshQName forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
generalizedFieldName forall a. [a] -> [a] -> [a]
++) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m String
getMetaNameSuggestion
  [Dom QName]
genRecFields <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. a -> Dom a
defaultDom forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> TCMT IO QName
mkFieldName) [MetaId]
sortedMetas
  QName
genRecName   <- String -> TCMT IO QName
freshQName String
"GeneralizeTel"
  ConHead
genRecCon    <- String -> TCMT IO QName
freshQName String
"mkGeneralizeTel" forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ QName
con -> ConHead
                  { conName :: QName
conName      = QName
con
                  , conDataRecord :: DataOrRecord
conDataRecord= PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching
                  , conInductive :: Induction
conInductive = Induction
Inductive
                  , conFields :: [Arg QName]
conFields    = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
genRecFields
                  }
  Int
projIx <- forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Int
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [MetaId]
sortedMetas [Dom QName]
genRecFields) forall a b. (a -> b) -> a -> b
$ \ (MetaId
meta, Dom QName
fld) -> do
    Type
fieldTy <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
meta
    let field :: QName
field = forall t e. Dom' t e -> e
unDom Dom QName
fld
    QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
field (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom QName
fld) QName
field Type
fieldTy forall a b. (a -> b) -> a -> b
$
      let proj :: Projection
proj = Projection { projProper :: Maybe QName
projProper   = forall a. a -> Maybe a
Just QName
genRecName
                            , projOrig :: QName
projOrig     = QName
field
                            , projFromType :: Arg QName
projFromType = forall a. a -> Arg a
defaultArg QName
genRecName
                            , projIndex :: Int
projIndex    = Int
projIx
                            , projLams :: ProjLams
projLams     = [Arg String] -> ProjLams
ProjLams [forall a. a -> Arg a
defaultArg String
"gtel"] } in
      Function { funClauses :: [Clause]
funClauses      = []
               , funCompiled :: Maybe CompiledClauses
funCompiled     = forall a. Maybe a
Nothing
               , funSplitTree :: Maybe SplitTree
funSplitTree    = forall a. Maybe a
Nothing
               , funTreeless :: Maybe Compiled
funTreeless     = forall a. Maybe a
Nothing
               , funInv :: FunctionInverse
funInv          = forall c. FunctionInverse' c
NotInjective
               , funMutual :: Maybe [QName]
funMutual       = forall a. a -> Maybe a
Just []
               , funAbstr :: IsAbstract
funAbstr        = IsAbstract
ConcreteDef
               , funDelayed :: Delayed
funDelayed      = Delayed
NotDelayed
               , funProjection :: Either ProjectionLikenessMissing Projection
funProjection   = forall a b. b -> Either a b
Right Projection
proj
               , funFlags :: Set FunctionFlag
funFlags        = forall a. Set a
Set.empty
               , funTerminates :: Maybe Bool
funTerminates   = forall a. a -> Maybe a
Just Bool
True
               , funExtLam :: Maybe ExtLamInfo
funExtLam       = forall a. Maybe a
Nothing
               , funWith :: Maybe QName
funWith         = forall a. Maybe a
Nothing
               , funCovering :: [Clause]
funCovering     = []
               , funIsKanOp :: Maybe QName
funIsKanOp      = forall a. Maybe a
Nothing
               }
  QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' (ConHead -> QName
conName ConHead
genRecCon) ArgInfo
defaultArgInfo (ConHead -> QName
conName ConHead
genRecCon) HasCallStack => Type
__DUMMY_TYPE__ forall a b. (a -> b) -> a -> b
$ -- Filled in later
    Constructor { conPars :: Int
conPars   = Int
0
                , conArity :: Int
conArity  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
genRecFields
                , conSrcCon :: ConHead
conSrcCon = ConHead
genRecCon
                , conData :: QName
conData   = QName
genRecName
                , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
                , conInd :: Induction
conInd    = Induction
Inductive
                , conComp :: CompKit
conComp   = CompKit
emptyCompKit
                , conProj :: Maybe [QName]
conProj   = forall a. Maybe a
Nothing
                , conForced :: [IsForced]
conForced = []
                , conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing
                }
  let dummyTel :: t -> Telescope
dummyTel t
0 = forall a. Tele a
EmptyTel
      dummyTel t
n = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (forall a. a -> Dom a
defaultDom HasCallStack => Type
__DUMMY_TYPE__) forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
Abs String
"_" forall a b. (a -> b) -> a -> b
$ t -> Telescope
dummyTel (t
n forall a. Num a => a -> a -> a
- t
1)
  QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
genRecName ArgInfo
defaultArgInfo QName
genRecName (Sort -> Type
sort Sort
genRecSort) forall a b. (a -> b) -> a -> b
$
    Record { recPars :: Int
recPars         = Int
0
           , recClause :: Maybe Clause
recClause       = forall a. Maybe a
Nothing
           , recConHead :: ConHead
recConHead      = ConHead
genRecCon
           , recNamedCon :: Bool
recNamedCon     = Bool
False
           , recFields :: [Dom QName]
recFields       = [Dom QName]
genRecFields
           , recTel :: Telescope
recTel          = forall {t}. (Eq t, Num t) => t -> Telescope
dummyTel (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
genRecFields) -- Filled in later
           , recMutual :: Maybe [QName]
recMutual       = forall a. a -> Maybe a
Just []
           , recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta -> EtaEquality
Inferred forall a. HasEta' a
YesEta
           , recPatternMatching :: PatternOrCopattern
recPatternMatching = PatternOrCopattern
CopatternMatching
           , recInduction :: Maybe Induction
recInduction    = forall a. Maybe a
Nothing
           , recTerminates :: Maybe Bool
recTerminates   = forall a. a -> Maybe a
Just Bool
True    -- not recursive
           , recAbstr :: IsAbstract
recAbstr        = IsAbstract
ConcreteDef
           , recComp :: CompKit
recComp         = CompKit
emptyCompKit
           }
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"created genRec" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom QName]
genRecFields) ]
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"created genRec" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Pretty a => a -> String
prettyShow [Dom QName]
genRecFields) ]
  -- Solve the genRecMeta
  Args
args <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let genRecTy :: Type
genRecTy = forall t a. Sort' t -> a -> Type'' t a
El Sort
genRecSort forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
genRecName forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args
  forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
genRecTy Type
genRecMeta
  forall (m :: * -> *) a. Monad m => a -> m a
return (QName
genRecName, ConHead
genRecCon, forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom QName]
genRecFields)

-- | Once we have the generalized telescope we can fill in the missing details of the record type.
fillInGenRecordDetails :: QName -> ConHead -> [QName] -> Type -> Telescope -> TCM ()
fillInGenRecordDetails :: QName -> ConHead -> [QName] -> Type -> Telescope -> TCMT IO ()
fillInGenRecordDetails QName
name ConHead
con [QName]
fields Type
recTy Telescope
fieldTel = do
  Telescope
cxtTel <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let fullTel :: Telescope
fullTel = Telescope
cxtTel forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
fieldTel
  -- Field types
  let mkFieldTypes :: [QName] -> Telescope -> [Type]
mkFieldTypes [] Telescope
EmptyTel = []
      mkFieldTypes (QName
fld : [QName]
flds) (ExtendTel Dom Type
ty Abs Telescope
ftel) =
          forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxtTel (forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (forall a. a -> Dom a
defaultDom Type
recTy) (forall a. String -> a -> Abs a
Abs String
"r" forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
ty)) forall a. a -> [a] -> [a]
:
          [QName] -> Telescope -> [Type]
mkFieldTypes [QName]
flds (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
ftel Term
proj)
        where
          s :: Sort
s = Dom Type -> Abs Type -> Sort
mkPiSort (forall a. a -> Dom a
defaultDom Type
recTy) (forall a. String -> a -> Abs a
Abs String
"r" forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
ty)
          proj :: Term
proj = Int -> Elims -> Term
Var Int
0 [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld]
      mkFieldTypes [QName]
_ Telescope
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
  let fieldTypes :: [Type]
fieldTypes = [QName] -> Telescope -> [Type]
mkFieldTypes [QName]
fields (forall a. Subst a => Int -> a -> a
raise Int
1 Telescope
fieldTel)
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Field types:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
fieldTypes)
  forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ forall {m :: * -> *}. MonadTCState m => QName -> Type -> m ()
setType [QName]
fields [Type]
fieldTypes
  -- Constructor type
  let conType :: Type
conType = Telescope
fullTel forall t. Abstract t => Telescope -> t -> t
`abstract` forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
fieldTel) Type
recTy
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.generalize" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Final genRecCon type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
conType)
  forall {m :: * -> *}. MonadTCState m => QName -> Type -> m ()
setType (ConHead -> QName
conName ConHead
con) Type
conType
  -- Record telescope: Includes both parameters and fields.
  forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
name forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set (Lens' Defn Definition
lensTheDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' RecordData Defn
lensRecord forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Telescope RecordData
lensRecTel) Telescope
fullTel
  where
    setType :: QName -> Type -> m ()
setType QName
q Type
ty = forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q forall a b. (a -> b) -> a -> b
$ \ Definition
d -> Definition
d { defType :: Type
defType = Type
ty }