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.IntMap as IntMap
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 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.List   (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)


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

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

  Telescope
tel' <- Substitution' (SubstArg Telescope) -> Telescope -> Telescope
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Telescope)
sub (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> TCMT IO Telescope
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 = (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (c -> b -> c
forall a b. a -> b -> a
const c
name) ((b, d) -> (c, d)) -> f (b, d) -> f (c, d)
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 <- m Name -> (Name -> m Name) -> Maybe Name -> m Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Name -> Name
forall a. LensInScope a => a -> a
setNotInScope (Name -> Name) -> m Name -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ b
s) Name -> m Name
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
mname
          Dom' t (Name, d) -> m (Dom' t (Name, d))
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom' t (Name, d) -> m (Dom' t (Name, d)))
-> Dom' t (Name, d) -> m (Dom' t (Name, d))
forall a b. (a -> b) -> a -> b
$ Name -> Dom' t (b, d) -> Dom' t (Name, d)
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  = (b, d) -> b
forall a b. (a, b) -> a
fst ((b, d) -> b) -> (b, d) -> b
forall a b. (a -> b) -> a -> b
$ Dom' t (b, d) -> (b, d)
forall t e. Dom' t e -> e
unDom Dom' t (b, d)
d
      dropCxt :: Impossible -> m a -> m a
dropCxt Impossible
err = Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext (Impossible -> Int -> Substitution
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
1) (Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. Int -> [a] -> [a]
drop Int
1)
  [Dom (Name, Type)]
genTelCxt <- Impossible
-> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)])
-> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
forall a b. (a -> b) -> a -> b
$ ((Maybe Name, Dom' Term (ArgName, Type))
 -> TCMT IO (Dom (Name, Type)))
-> [(Maybe Name, Dom' Term (ArgName, Type))]
-> TCMT IO [Dom (Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe Name, Dom' Term (ArgName, Type))
-> TCMT IO (Dom (Name, Type))
forall (m :: * -> *) b t d.
(FreshName b, MonadFresh NameId m) =>
(Maybe Name, Dom' t (b, d)) -> m (Dom' t (Name, d))
cxtEntry ([(Maybe Name, Dom' Term (ArgName, Type))]
 -> TCMT IO [Dom (Name, Type)])
-> [(Maybe Name, Dom' Term (ArgName, Type))]
-> TCMT IO [Dom (Name, Type)]
forall a b. (a -> b) -> a -> b
$ [(Maybe Name, Dom' Term (ArgName, Type))]
-> [(Maybe Name, Dom' Term (ArgName, Type))]
forall a. [a] -> [a]
reverse ([(Maybe Name, Dom' Term (ArgName, Type))]
 -> [(Maybe Name, Dom' Term (ArgName, Type))])
-> [(Maybe Name, Dom' Term (ArgName, Type))]
-> [(Maybe Name, Dom' Term (ArgName, Type))]
forall a b. (a -> b) -> a -> b
$ [Maybe Name]
-> [Dom' Term (ArgName, Type)]
-> [(Maybe Name, Dom' Term (ArgName, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Name]
genTelVars ([Dom' Term (ArgName, Type)]
 -> [(Maybe Name, Dom' Term (ArgName, Type))])
-> [Dom' Term (ArgName, Type)]
-> [(Maybe Name, Dom' Term (ArgName, Type))]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
genTel

  -- For the explicit module telescope we get the names from the typecheck
  -- action.
  let newTelCxt :: [Dom (Name, Type)]
newTelCxt = (Name -> Dom' Term (ArgName, Type) -> Dom (Name, Type))
-> [Name] -> [Dom' Term (ArgName, Type)] -> [Dom (Name, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Dom' Term (ArgName, Type) -> Dom (Name, Type)
forall (f :: * -> *) c b d. Functor f => c -> f (b, d) -> f (c, d)
setName [Name]
cxtNames ([Dom' Term (ArgName, Type)] -> [Dom (Name, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom (Name, Type)]
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a]
reverse ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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' <- Substitution' (SubstArg [(Name, (Term, Dom Type))])
-> [(Name, (Term, Dom Type))] -> [(Name, (Term, Dom Type))]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Substitution
sub) ([(Name, (Term, Dom Type))] -> [(Name, (Term, Dom Type))])
-> TCMT IO [(Name, (Term, Dom Type))]
-> TCMT IO [(Name, (Term, Dom Type))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, (Term, Dom Type))] -> TCMT IO [(Name, (Term, Dom Type))]
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)) = Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
x Term
v Dom Type
dom

  Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext Substitution
sub (([Dom (Name, Type)]
genTelCxt [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. [a] -> [a] -> [a]
++) ([Dom (Name, Type)] -> [Dom (Name, Type)])
-> ([Dom (Name, Type)] -> [Dom (Name, Type)])
-> [Dom (Name, Type)]
-> [Dom (Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. Int -> [a] -> [a]
drop Int
1) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
    Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext (Int -> Substitution
forall a. Int -> Substitution' a
raiseS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel')) ([Dom (Name, Type)]
newTelCxt [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. [a] -> [a] -> [a]
++) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
      ((Name, (Term, Dom Type)) -> TCM a -> TCM a)
-> TCM a -> [(Name, (Term, Dom Type))] -> TCM a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, (Term, Dom Type)) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, (Term, Dom Type)) -> m a -> m a
addLet ([Maybe Name] -> Telescope -> TCM a
ret [Maybe Name]
genTelVars (Telescope -> TCM a) -> Telescope -> TCM a
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope -> Telescope
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, ()
_) <- Set QName -> TCM (Type, ()) -> TCM ([Maybe QName], Type, ())
forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s (TCM (Type, ()) -> TCM ([Maybe QName], Type, ()))
-> TCM (Type, ()) -> TCM ([Maybe QName], Type, ())
forall a b. (a -> b) -> a -> b
$ (,()) (Type -> (Type, ())) -> TCM Type -> TCM (Type, ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
typecheckAction
  ([Maybe QName], Type) -> TCM ([Maybe QName], Type)
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' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s TCM (Type, a)
typecheckAction = Account (BenchPhase (TCMT IO))
-> TCM ([Maybe QName], Type, a) -> TCM ([Maybe QName], Type, a)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo [BenchPhase (TCMT IO)
Phase
Typing, BenchPhase (TCMT IO)
Phase
Generalize] (TCM ([Maybe QName], Type, a) -> TCM ([Maybe QName], Type, a))
-> TCM ([Maybe QName], Type, a) -> TCM ([Maybe QName], Type, a)
forall a b. (a -> b) -> a -> b
$ (Type -> TCM ([Maybe QName], Type, a))
-> TCM ([Maybe QName], Type, a)
forall a. (Type -> TCM a) -> TCM a
withGenRecVar ((Type -> TCM ([Maybe QName], Type, a))
 -> TCM ([Maybe QName], Type, a))
-> (Type -> TCM ([Maybe QName], Type, a))
-> TCM ([Maybe QName], Type, a)
forall a b. (a -> b) -> a -> b
$ \ Type
genRecMeta -> do

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

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

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

  ([Maybe QName], Type, a) -> TCM ([Maybe QName], Type, a)
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, MetaStore)
createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore)
createMetasAndTypeCheck Set QName
s TCM a
typecheckAction = do
  ((Map MetaId QName
namedMetas, a
x), MetaStore
allmetas) <- TCMT IO (Map MetaId QName, a)
-> TCMT IO ((Map MetaId QName, a), MetaStore)
forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy (TCMT IO (Map MetaId QName, a)
 -> TCMT IO ((Map MetaId QName, a), MetaStore))
-> TCMT IO (Map MetaId QName, a)
-> TCMT IO ((Map MetaId QName, a), MetaStore)
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 <- Lens' (Map QName GeneralizedValue) TCEnv
-> (Map QName GeneralizedValue -> Map QName GeneralizedValue)
-> TCM a
-> TCM a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map QName GeneralizedValue) TCEnv
eGeneralizedVars (Map QName GeneralizedValue
-> Map QName GeneralizedValue -> Map QName GeneralizedValue
forall a b. a -> b -> a
const Map QName GeneralizedValue
genvals) TCM a
typecheckAction
    (Map MetaId QName, a) -> TCMT IO (Map MetaId QName, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map MetaId QName
metamap, a
x)
  (a, Map MetaId QName, MetaStore)
-> TCM (a, Map MetaId QName, MetaStore)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, Map MetaId QName
namedMetas, MetaStore
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 :: (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)
  Dom' Term (ArgName, Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ((ArgName, Type) -> Dom' Term (ArgName, Type)
forall a. a -> Dom a
defaultDom (ArgName
"genTel" :: String, Type
genRecMeta)) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ Type -> TCM a
ret Type
genRecMeta

-- | Compute the generalized telescope from metas created when checking the type/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 -> Map MetaId name -> MetaStore ->
  TCM (Telescope, [Maybe name], Substitution)
computeGeneralization :: Type
-> Map MetaId name
-> MetaStore
-> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization Type
genRecMeta Map MetaId name
nameMap MetaStore
allmetas = TCM (Telescope, [Maybe name], Substitution)
-> TCM (Telescope, [Maybe name], Substitution)
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCM (Telescope, [Maybe name], Substitution)
 -> TCM (Telescope, [Maybe name], Substitution))
-> TCM (Telescope, [Maybe name], Substitution)
-> TCM (Telescope, [Maybe name], Substitution)
forall a b. (a -> b) -> a -> b
$ do

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

  -- Pair metas with their metaInfo
  [(MetaId, MetaVariable)]
mvs <- (Int -> TCMT IO (MetaId, MetaVariable))
-> [Int] -> TCMT IO [(MetaId, MetaVariable)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((\ MetaId
x -> (MetaId
x,) (MetaVariable -> (MetaId, MetaVariable))
-> TCMT IO MetaVariable -> TCMT IO (MetaId, MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x) (MetaId -> TCMT IO (MetaId, MetaVariable))
-> (Int -> MetaId) -> Int -> TCMT IO (MetaId, MetaVariable)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MetaId
MetaId) ([Int] -> TCMT IO [(MetaId, MetaVariable)])
-> [Int] -> TCMT IO [(MetaId, MetaVariable)]
forall a b. (a -> b) -> a -> b
$ MetaStore -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys MetaStore
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 <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  let isFreshMeta :: (MetaId, MetaVariable) -> TCMT IO Bool
isFreshMeta (MetaId
x,MetaVariable
mv) = MetaVariable -> (Range -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> TCMT IO Bool) -> TCMT IO Bool)
-> (Range -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \ Range
_ -> Maybe Substitution -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Substitution -> Bool)
-> TCMT IO (Maybe Substitution) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckpointId -> TCMT IO (Maybe Substitution)
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe Substitution)
checkpointSubstitution' CheckpointId
cp
  [(MetaId, MetaVariable)]
mvs <- ((MetaId, MetaVariable) -> TCMT IO Bool)
-> [(MetaId, MetaVariable)] -> TCMT IO [(MetaId, MetaVariable)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (MetaId, MetaVariable) -> TCMT IO Bool
isFreshMeta [(MetaId, MetaVariable)]
mvs
  [ProblemConstraint]
cs <- [ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint]
forall a. [a] -> [a] -> [a]
(++) ([ProblemConstraint] -> [ProblemConstraint] -> [ProblemConstraint])
-> TCMT IO [ProblemConstraint]
-> TCMT IO ([ProblemConstraint] -> [ProblemConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stAwakeConstraints
             TCMT IO ([ProblemConstraint] -> [ProblemConstraint])
-> TCMT IO [ProblemConstraint] -> TCMT IO [ProblemConstraint]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Lens' [ProblemConstraint] TCState -> TCMT IO [ProblemConstraint]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [ProblemConstraint] TCState
stSleepingConstraints

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

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

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

  let isConstrained :: MetaId -> Bool
isConstrained MetaId
x = MetaId -> Set MetaId -> Bool
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) = MetaId -> Map MetaId name -> Bool
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 DoGeneralize -> DoGeneralize -> Bool
forall a. Eq a => a -> a -> Bool
/= Arg DoGeneralize -> DoGeneralize
forall e. Arg e -> e
unArg (MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv))
      isSort :: (a, MetaVariable) -> Bool
isSort = MetaVariable -> Bool
isSortMeta_ (MetaVariable -> Bool)
-> ((a, MetaVariable) -> MetaVariable) -> (a, MetaVariable) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, MetaVariable) -> MetaVariable
forall a b. (a, b) -> b
snd
      isOpen :: (a, MetaVariable) -> Bool
isOpen = MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool)
-> ((a, MetaVariable) -> MetaInstantiation)
-> (a, MetaVariable)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> ((a, MetaVariable) -> MetaVariable)
-> (a, MetaVariable)
-> MetaInstantiation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, MetaVariable) -> MetaVariable
forall a b. (a, b) -> b
snd

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

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

  -- Issue 3301: We can't generalize over sorts
  [(MetaId, MetaVariable)]
-> ([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [(MetaId, MetaVariable)]
openSortMetas (([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ())
-> ([(MetaId, MetaVariable)] -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ [(MetaId, MetaVariable)]
ms ->
    Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [MetaId] -> Warning
CantGeneralizeOverSorts ([MetaId] -> Warning) -> [MetaId] -> Warning
forall a b. (a -> b) -> a -> b
$ ((MetaId, MetaVariable) -> MetaId)
-> [(MetaId, MetaVariable)] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map (MetaId, MetaVariable) -> MetaId
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 <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
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 = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      canGeneralize MetaId
x = do
          MetaVariable
mv   <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
          Maybe Substitution
msub <- MetaVariable
-> (Range -> TCMT IO (Maybe Substitution))
-> TCMT IO (Maybe Substitution)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> TCMT IO (Maybe Substitution))
 -> TCMT IO (Maybe Substitution))
-> (Range -> TCMT IO (Maybe Substitution))
-> TCMT IO (Maybe Substitution)
forall a b. (a -> b) -> a -> b
$ \ Range
_ ->
                    CheckpointId -> TCMT IO (Maybe Substitution)
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 [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int
0 .. Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
                  (Just (Wk Int
n Substitution
IdS), Perm Int
m [Int]
xs) -> [Int]
xs [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int
0 .. Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
                  (Maybe Substitution, Permutation)
_                            -> Bool
False
          Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
sameContext (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
            Type
ty <- MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
x
            let Perm Int
m [Int]
xs = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
            ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Don't know how to generalize over"
              , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty
              , ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"in context"
              , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc)
-> (Telescope -> TCM Doc) -> Telescope -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
              , ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"permutation:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ((Int, [Int]) -> ArgName
forall a. Show a => a -> ArgName
show (Int
m, [Int]
xs))
              , ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"subst:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe Substitution
msub ]
          Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sameContext
  Set MetaId
inherited <- ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (TCMT IO [Set MetaId] -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ [(MetaId, MetaVariable)]
-> ((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(MetaId, MetaVariable)]
generalizableClosed (((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
 -> TCMT IO [Set MetaId])
-> ((MetaId, MetaVariable) -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall a b. (a -> b) -> a -> b
$ \ (MetaId
x, MetaVariable
mv) ->
    case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
      InstV [Arg ArgName]
_ Term
v -> do
        ArgName
parentName <- MetaId -> TCMT IO ArgName
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
x
        [MetaId]
metas <- (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
canGeneralize ([MetaId] -> TCMT IO [MetaId])
-> (Term -> [MetaId]) -> Term -> TCMT IO [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId])
-> (Term -> Set MetaId) -> Term -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Set MetaId) -> Term -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term -> TCMT IO [MetaId]) -> TCMT IO Term -> TCMT IO [MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v
        let suggestNames :: Integer -> [MetaId] -> TCMT IO ()
suggestNames Integer
i [] = () -> TCMT IO ()
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 :: ArgName
suf | [MetaId] -> Bool
forall a. Null a => a -> Bool
null [MetaId]
ms Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1, MetaV{} <- Term
v = ArgName
""
                      | Bool
otherwise                       = ArgName
"." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
i
              MetaId -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
m (ArgName
parentName ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
suf)
              Integer -> [MetaId] -> TCMT IO ()
suggestNames (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) [MetaId]
ms
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([MetaId] -> Bool
forall a. Null a => a -> Bool
null [MetaId]
metas) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat [TCM Doc
"Inherited metas from ", MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x, TCM Doc
":"] TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> TCM Doc) -> [MetaId] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [MetaId]
metas)
                                    -- Don't suggest names for explicitly named generalizable metas
        [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas Set MetaId -> TCMT IO () -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Integer -> [MetaId] -> TCMT IO ()
suggestNames Integer
1 ((MetaId -> Bool) -> [MetaId] -> [MetaId]
forall a. (a -> Bool) -> [a] -> [a]
filter (MetaId -> Map MetaId name -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map MetaId name
nameMap) [MetaId]
metas)
      MetaInstantiation
_ -> TCMT IO (Set MetaId)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"we're generalizing over" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((MetaId -> TCM Doc) -> [MetaId] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> TCM Doc
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 <- TCMT IO [MetaId] -> TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId]
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> TCMT IO [MetaId]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
GeneralizeCyclicDependency) (TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId])
-> TCMT IO (Maybe [MetaId]) -> TCMT IO [MetaId]
forall a b. (a -> b) -> a -> b
$
    [MetaId] -> TCMT IO (Maybe [MetaId])
dependencySortMetas ([MetaId]
generalizeOver [MetaId] -> [MetaId] -> [MetaId]
forall a. [a] -> [a] -> [a]
++ [MetaId]
reallyDontGeneralize [MetaId] -> [MetaId] -> [MetaId]
forall a. [a] -> [a] -> [a]
++ ((MetaId, MetaVariable) -> MetaId)
-> [(MetaId, MetaVariable)] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map (MetaId, MetaVariable) -> MetaId
forall a b. (a, b) -> a
fst [(MetaId, MetaVariable)]
openSortMetas)
  let sortedMetas :: [MetaId]
sortedMetas = (MetaId -> Bool) -> [MetaId] -> [MetaId]
forall a. (a -> Bool) -> [a] -> [a]
filter MetaId -> Bool
shouldGeneralize [MetaId]
allSortedMetas

  let dropCxt :: Impossible -> m a -> m a
dropCxt Impossible
err = Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext (Impossible -> Int -> Substitution
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
1) (Int -> [Dom (Name, Type)] -> [Dom (Name, Type)]
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) <- Impossible
-> TCMT IO (QName, ConHead, [QName])
-> TCMT IO (QName, ConHead, [QName])
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (TCMT IO (QName, ConHead, [QName])
 -> TCMT IO (QName, ConHead, [QName]))
-> TCMT IO (QName, ConHead, [QName])
-> TCMT IO (QName, ConHead, [QName])
forall a b. (a -> b) -> a -> b
$
      Type -> [MetaId] -> TCMT IO (QName, ConHead, [QName])
createGenRecordType Type
genRecMeta [MetaId]
sortedMetas

  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
    [ TCM Doc
"created genRecordType"
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"genRecName   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
genRecName
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"genRecCon    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
genRecCon
    , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"genRecFields = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((QName -> TCM Doc) -> [QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> TCM Doc
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 <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let solve :: MetaId -> QName -> TCMT IO ()
solve MetaId
m QName
field = do
        ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"solving generalized meta" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
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.
        TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCMT IO Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
m) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        MetaId -> [Arg ArgName] -> Term -> TCMT IO ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm' MetaId
m (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
cxtTel) (Term -> TCMT IO ()) -> Term -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
field]
  (MetaId -> QName -> TCMT IO ())
-> [MetaId] -> [QName] -> TCMT IO ()
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 = (MetaId -> Maybe name) -> [MetaId] -> [Maybe name]
forall a b. (a -> b) -> [a] -> [b]
map (MetaId -> Map MetaId name -> Maybe name
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 ArgName, Type)]
teleTypes <- do
    Args
args <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    ([[(Arg ArgName, Type)]] -> [(Arg ArgName, Type)])
-> TCMT IO [[(Arg ArgName, Type)]] -> TCMT IO [(Arg ArgName, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(Arg ArgName, Type)]] -> [(Arg ArgName, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (TCMT IO [[(Arg ArgName, Type)]] -> TCMT IO [(Arg ArgName, Type)])
-> TCMT IO [[(Arg ArgName, Type)]] -> TCMT IO [(Arg ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ [MetaId]
-> (MetaId -> TCMT IO [(Arg ArgName, Type)])
-> TCMT IO [[(Arg ArgName, Type)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
sortedMetas ((MetaId -> TCMT IO [(Arg ArgName, Type)])
 -> TCMT IO [[(Arg ArgName, Type)]])
-> (MetaId -> TCMT IO [(Arg ArgName, Type)])
-> TCMT IO [[(Arg ArgName, Type)]]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
      MetaVariable
mv   <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      let info :: ArgInfo
info =
            ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
hideOrKeepInstance (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$
            Arg DoGeneralize -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (Arg DoGeneralize -> ArgInfo) -> Arg DoGeneralize -> ArgInfo
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaInfo -> Arg DoGeneralize) -> MetaInfo -> Arg DoGeneralize
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' <- Type -> Args -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
t (Args -> TCM Type) -> Args -> TCM Type
forall a b. (a -> b) -> a -> b
$ Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
perm) Args
args
      [(Arg ArgName, Type)] -> TCMT IO [(Arg ArgName, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (ArgName -> Arg ArgName) -> ArgName -> Arg ArgName
forall a b. (a -> b) -> a -> b
$ MetaInfo -> ArgName
miNameSuggestion (MetaInfo -> ArgName) -> MetaInfo -> ArgName
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv, Type
t')]
  let genTel :: Telescope
genTel = ConHead -> [(Arg ArgName, Type)] -> Telescope
buildGeneralizeTel ConHead
genRecCon [(Arg ArgName, Type)]
teleTypes

  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"genTel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM 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})
        | Int -> MetaStore -> Bool
forall a. Int -> IntMap a -> Bool
IntMap.member (MetaId -> Int
metaId MetaId
x) MetaStore
allmetas = (MetaId, InteractionId) -> Maybe (MetaId, InteractionId)
forall a. a -> Maybe a
Just (MetaId
x, InteractionId
ii)
      inscope (InteractionId, InteractionPoint)
_ = Maybe (MetaId, InteractionId)
forall a. Maybe a
Nothing
  Map MetaId InteractionId
ips <- [(MetaId, InteractionId)] -> Map MetaId InteractionId
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(MetaId, InteractionId)] -> Map MetaId InteractionId)
-> (BiMap InteractionId InteractionPoint
    -> [(MetaId, InteractionId)])
-> BiMap InteractionId InteractionPoint
-> Map MetaId InteractionId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, InteractionPoint)
 -> Maybe (MetaId, InteractionId))
-> [(InteractionId, InteractionPoint)] -> [(MetaId, InteractionId)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe (MetaId, InteractionId)
inscope ([(InteractionId, InteractionPoint)] -> [(MetaId, InteractionId)])
-> (BiMap InteractionId InteractionPoint
    -> [(InteractionId, InteractionPoint)])
-> BiMap InteractionId InteractionPoint
-> [(MetaId, InteractionId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
-> [(InteractionId, InteractionPoint)]
forall a b. (a, b) -> a
fst (([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
 -> [(InteractionId, InteractionPoint)])
-> (BiMap InteractionId InteractionPoint
    -> ([(InteractionId, InteractionPoint)],
        [(MetaId, InteractionId)]))
-> BiMap InteractionId InteractionPoint
-> [(InteractionId, InteractionPoint)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BiMap InteractionId InteractionPoint
-> ([(InteractionId, InteractionPoint)], [(MetaId, InteractionId)])
forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
BiMap.toDistinctAscendingLists (BiMap InteractionId InteractionPoint -> Map MetaId InteractionId)
-> TCMT IO (BiMap InteractionId InteractionPoint)
-> TCMT IO (Map MetaId InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (BiMap InteractionId InteractionPoint) TCState
-> TCMT IO (BiMap InteractionId InteractionPoint)
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.
  Impossible -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> m a -> m a
dropCxt Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
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 (((Arg ArgName, Type) -> ArgInfo)
-> [(Arg ArgName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Arg ArgName -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo (Arg ArgName -> ArgInfo)
-> ((Arg ArgName, Type) -> Arg ArgName)
-> (Arg ArgName, Type)
-> ArgInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg ArgName, Type) -> Arg ArgName
forall a b. (a, b) -> a
fst) [(Arg ArgName, Type)]
teleTypes) ([(Arg ArgName, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Arg ArgName, Type)]
teleTypes)

  (Telescope, [Maybe name], Substitution)
-> TCM (Telescope, [Maybe name], Substitution)
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
  | (MetaId -> Bool) -> [MetaId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all MetaId -> Bool
isGeneralized [MetaId]
metas = () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise               = [Dom' Term (ArgName, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [] Telescope
genTel [MetaId]
metas
  where
    prune :: [Dom' Term (ArgName, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [Dom' Term (ArgName, Type)]
_ Telescope
_ [] = () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    prune [Dom' Term (ArgName, 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.
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
        MetaId
x <- if Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then MetaId -> TCMT IO MetaId
prePrune MetaId
x
                             else MetaId -> TCMT IO MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x
        Telescope -> MetaId -> TCMT IO ()
pruneMeta ([Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> [Dom' Term (ArgName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a]
reverse [Dom' Term (ArgName, Type)]
cxt) MetaId
x
      [Dom' Term (ArgName, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune [Dom' Term (ArgName, Type)]
cxt Telescope
tel [MetaId]
xs
    prune [Dom' Term (ArgName, Type)]
cxt (ExtendTel Dom Type
a Abs Telescope
tel) (MetaId
x : [MetaId]
xs) = [Dom' Term (ArgName, Type)] -> Telescope -> [MetaId] -> TCMT IO ()
prune ((Type -> (ArgName, Type)) -> Dom Type -> Dom' Term (ArgName, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName
x,) Dom Type
a Dom' Term (ArgName, Type)
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. a -> [a] -> [a]
: [Dom' Term (ArgName, Type)]
cxt) (Abs Telescope -> Telescope
forall a. Abs a -> a
unAbs Abs Telescope
tel) [MetaId]
xs
      where x :: ArgName
x = Abs Telescope -> ArgName
forall a. Abs a -> ArgName
absName Abs Telescope
tel
    prune [Dom' Term (ArgName, Type)]
_ Telescope
_ [MetaId]
_ = TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

    prepruneError :: String -> MetaId -> TCM a
    prepruneError :: ArgName -> MetaId -> TCM a
prepruneError ArgName
msg MetaId
x = do
      Range
r <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x
      Doc -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords (ArgName
msg ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" The problematic unsolved meta is") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
                 (Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x []) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"at" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> TCM 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 <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
      MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
      (Int
i, Maybe Type
_A) <- MetaVariable
-> (Range -> TCMT IO (Int, Maybe Type))
-> TCMT IO (Int, Maybe Type)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> TCMT IO (Int, Maybe Type)) -> TCMT IO (Int, Maybe Type))
-> (Range -> TCMT IO (Int, Maybe Type))
-> TCMT IO (Int, Maybe Type)
forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do
        Substitution
δ <- CheckpointId -> TCMT IO Substitution
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm Substitution
checkpointSubstitution CheckpointId
cp
        Maybe Type
_A <- case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
                IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
                HasType{} -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> TCM Type -> TCMT IO (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
x
        case Substitution
δ of
          Wk Int
n Substitution
IdS -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, Maybe Type
_A)
          Substitution
IdS      -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
0, Maybe Type
_A)
          Substitution
_        -> MetaId -> TCMT IO (Int, Maybe Type)
forall a. MetaId -> TCM a
prepruneErrorRefinedContext MetaId
x
      if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then MetaId -> TCMT IO MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x else do
        ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize.prune.pre" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"prepruning"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"|Δ| =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCM 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 (Maybe Type -> IntSet
forall t. Free t => t -> IntSet
allFreeVars Maybe Type
_A) of
          Just (Int
j, IntSet
_) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i -> MetaId -> TCMT IO ()
forall a. MetaId -> TCM a
prepruneErrorCyclicDependencies MetaId
x
          Maybe (Int, IntSet)
_                   -> () -> TCMT IO ()
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
ρ  = Impossible -> Int -> Substitution
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Int
i
            ρ' :: Substitution
ρ' = Int -> 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ρ' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
ρ' Term
u

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

        -- To solve it we enter the context of x again
        MetaVariable -> (Range -> TCMT IO MetaId) -> TCMT IO MetaId
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> TCMT IO MetaId) -> TCMT IO MetaId)
-> (Range -> TCMT IO MetaId) -> TCMT IO MetaId
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 (Sort -> Term) -> (Args -> Sort) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> (Args -> Elims) -> Args -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
                 Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
          TCMT IO () -> TCMT IO ()
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ρ') TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> MetaId -> TCMT IO ()
forall a. MetaId -> TCM a
prepruneErrorFailedToInstantiate MetaId
x
          MetaId -> MetaId -> TCMT IO ()
setInteractionPoint MetaId
x MetaId
y
          MetaId -> TCMT IO MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
y

    pruneMeta :: Telescope -> MetaId -> TCMT IO ()
pruneMeta Telescope
_Θ MetaId
x = do
      CheckpointId
cp <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
      MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta 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.
      MetaVariable -> (Range -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv ((Range -> TCMT IO ()) -> TCMT IO ())
-> (Range -> TCMT IO ()) -> TCMT IO ()
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.
        TCMT IO (Maybe Int) -> (Int -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Monad m =>
m (Maybe a) -> (a -> m ()) -> m ()
whenJustM (MetaVariable -> TCMT IO (Maybe Int)
findGenRec MetaVariable
mv) ((Int -> TCMT IO ()) -> TCMT IO ())
-> (Int -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do

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

        Telescope
_ΓrΔ <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
        let (Telescope
_Γ, Telescope
_Δ) = ([Dom' Term (ArgName, Type)] -> Telescope
telFromList [Dom' Term (ArgName, Type)]
gs, [Dom' Term (ArgName, Type)] -> Telescope
telFromList [Dom' Term (ArgName, Type)]
ds)
              where ([Dom' Term (ArgName, Type)]
gs, Dom' Term (ArgName, Type)
_ : [Dom' Term (ArgName, Type)]
ds) = Int
-> [Dom' Term (ArgName, Type)]
-> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
_ΓrΔ Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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{}  -> Maybe Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
                HasType{} -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> TCM Type -> TCMT IO (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins 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
δ <- CheckpointId -> TCMT IO 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 (Sort -> Term) -> (Args -> Sort) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort) -> (Args -> Elims) -> Args -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
               Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> TCMT IO Args -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO Args
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 (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
_Θ)
            --    Γ <- Γ (r : GenTel) Δ <- Γ₀ (r : GenTel) <- Γ₀
            γ :: Substitution
γ   = Impossible -> Int -> Substitution
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
δ Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution
forall a. Int -> Substitution' a
raiseS Int
1
            _Θγ :: Telescope
_Θγ = Substitution' (SubstArg Telescope) -> Telescope -> Telescope
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Telescope)
γ Telescope
_Θ
            _Δσ :: Telescope
_Δσ = Substitution' (SubstArg Telescope) -> Telescope -> Telescope
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Telescope)
σ Telescope
_Δ

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

        ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize.prune" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"Γ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Γ
          , TCM Doc
"Θ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Θ
          , TCM Doc
"Δ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Δ
          , TCM Doc
"σ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
σ
          , TCM Doc
"γ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
γ
          , TCM Doc
"δ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
δ
          , TCM Doc
"ρ   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
ρ
          , TCM Doc
"ρ⁻¹ =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
ρ'
          , TCM Doc
"Θγ  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Θγ
          , TCM Doc
"Δσ  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
_Δσ
          , TCM Doc
"_A  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe Type -> TCM 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 Θ.
        ([Dom (Name, Type)]
newCxt, [Dom (Name, Type)]
rΘ) <- do
          ([Dom (Name, Type)]
rΔ, Dom (Name, Type)
_ : [Dom (Name, Type)]
rΓ) <- Int
-> [Dom (Name, Type)] -> ([Dom (Name, Type)], [Dom (Name, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i ([Dom (Name, Type)] -> ([Dom (Name, Type)], [Dom (Name, Type)]))
-> TCMT IO [Dom (Name, Type)]
-> TCMT IO ([Dom (Name, Type)], [Dom (Name, Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
          let setName :: Dom' Term (ArgName, t) -> TCMT IO (Dom' Term (Name, t))
setName = ((ArgName, t) -> TCMT IO (Name, t))
-> Dom' Term (ArgName, t) -> TCMT IO (Dom' Term (Name, t))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((ArgName, t) -> TCMT IO (Name, t))
 -> Dom' Term (ArgName, t) -> TCMT IO (Dom' Term (Name, t)))
-> ((ArgName, t) -> TCMT IO (Name, t))
-> Dom' Term (ArgName, t)
-> TCMT IO (Dom' Term (Name, t))
forall a b. (a -> b) -> a -> b
$ \ (ArgName
s, t
ty) -> (,t
ty) (Name -> (Name, t)) -> TCMT IO Name -> TCMT IO (Name, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ArgName
s
          [Dom (Name, Type)]
rΘ <- (Dom' Term (ArgName, Type) -> TCMT IO (Dom (Name, Type)))
-> [Dom' Term (ArgName, Type)] -> TCMT IO [Dom (Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Dom' Term (ArgName, Type) -> TCMT IO (Dom (Name, Type))
forall t. Dom' Term (ArgName, t) -> TCMT IO (Dom' Term (Name, t))
setName ([Dom' Term (ArgName, Type)] -> TCMT IO [Dom (Name, Type)])
-> [Dom' Term (ArgName, Type)] -> TCMT IO [Dom (Name, Type)]
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a]
reverse ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
_Θγ
          let rΔσ :: [Dom (Name, Type)]
rΔσ = (Name -> Dom' Term (ArgName, Type) -> Dom (Name, Type))
-> [Name] -> [Dom' Term (ArgName, Type)] -> [Dom (Name, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Name
name Dom' Term (ArgName, Type)
dom -> (ArgName -> Name) -> (ArgName, Type) -> (Name, Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Name -> ArgName -> Name
forall a b. a -> b -> a
const Name
name) ((ArgName, Type) -> (Name, Type))
-> Dom' Term (ArgName, Type) -> Dom (Name, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (ArgName, Type)
dom)
                            ((Dom (Name, Type) -> Name) -> [Dom (Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) [Dom (Name, Type)]
rΔ)
                            ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. [a] -> [a]
reverse ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
_Δσ)
          ([Dom (Name, Type)], [Dom (Name, Type)])
-> TCMT IO ([Dom (Name, Type)], [Dom (Name, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dom (Name, Type)]
rΔσ [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. [a] -> [a] -> [a]
++ [Dom (Name, Type)]
rΘ [Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a. [a] -> [a] -> [a]
++ [Dom (Name, Type)]
rΓ, [Dom (Name, Type)]
rΘ)

        -- Now we can enter the new context and create our meta variable.
        (MetaId
y, Term
u) <- Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)])
-> TCM (MetaId, Term)
-> TCM (MetaId, Term)
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext Substitution
ρ ([Dom (Name, Type)] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a b. a -> b -> a
const [Dom (Name, Type)]
newCxt) (TCM (MetaId, Term) -> TCM (MetaId, Term))
-> TCM (MetaId, Term) -> TCM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ TCM (MetaId, Term) -> TCM (MetaId, Term)
forall a. TCM a -> TCM a
localScope (TCM (MetaId, Term) -> TCM (MetaId, Term))
-> TCM (MetaId, Term) -> TCM (MetaId, Term)
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).
          Int -> TCMT IO () -> TCMT IO ()
forall a. Int -> ScopeM a -> ScopeM a
outsideLocalVars Int
i (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Dom (Name, Type)] -> TCMT IO ()
forall (t :: * -> *) t b.
Foldable t =>
t (Dom' t (Name, b)) -> TCMT IO ()
addNamedVariablesToScope [Dom (Name, Type)]
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ρ' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
ρ' Term
u
        ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize.prune" Int
80 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"solving"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v   TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"=="
                         , Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
uρ' TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                         , Maybe Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe Type
_A ] ]
        TCMT IO () -> TCMT IO ()
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ρ') TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
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

        ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize.prune" Int
80 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCM Doc
"solved"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"v    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v)
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"uρ⁻¹ =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
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 -> TCMT IO (Maybe Int)
findGenRec MetaVariable
mv = do
      [Dom (Name, Type)]
cxt <- [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)])
-> TCMT IO [Dom (Name, Type)] -> TCMT IO [Dom (Name, Type)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
      let notPruned :: [Int]
notPruned = Permutation -> [Int] -> [Int]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP ([Dom (Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom (Name, Type)]
cxt) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
               [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int -> Dom (Name, Type) -> Int)
-> [Int] -> [Dom (Name, Type)] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom (Name, Type) -> Int
forall a b. a -> b -> a
const [Int
0..] [Dom (Name, Type)]
cxt
      case [ Int
i | (Int
i, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (Name
_, El Sort
_ (Def QName
q Elims
_))}) <- [Int] -> [Dom (Name, Type)] -> [(Int, Dom (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Dom (Name, Type)]
cxt,
                 QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
genRecName, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
notPruned ] of
        []    -> Maybe Int -> TCMT IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
        Int
_:Int
_:[Int]
_ -> TCMT IO (Maybe Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
        [Int
i]   -> Maybe Int -> TCMT IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe Int
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 = MetaVariable -> TCM (MetaId, Term) -> TCM (MetaId, Term)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange MetaVariable
mv (TCM (MetaId, Term) -> TCM (MetaId, Term))
-> TCM (MetaId, Term) -> TCM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
      case Maybe Type
mA of
        Maybe Type
Nothing -> do
          s :: Sort
s@(MetaS MetaId
y Elims
_) <- TCMT IO Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
          (MetaId, Term) -> TCM (MetaId, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId
y, Sort -> Term
Sort Sort
s)
        Just Type
_A -> do
          let _Aρ :: Type
_Aρ = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
ρ Type
_A
          RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck
                            (MetaInfo -> ArgName
miNameSuggestion (MetaInfo -> ArgName) -> MetaInfo -> ArgName
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
                            (Judgement MetaId -> Comparison
forall a. Judgement a -> Comparison
jComparison (Judgement MetaId -> Comparison) -> Judgement MetaId -> Comparison
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 =
      Maybe InteractionId -> (InteractionId -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (MetaId -> Map MetaId InteractionId -> Maybe InteractionId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MetaId
x Map MetaId InteractionId
interactionPoints) (InteractionId -> MetaId -> TCMT IO ()
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 (CompareAs -> TCMT IO ()) -> CompareAs -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ CompareAs -> (Type -> CompareAs) -> Maybe Type -> CompareAs
forall b a. b -> (a -> b) -> Maybe a -> b
maybe CompareAs
AsTypes Type -> CompareAs
AsTermsOf Maybe Type
mt
        Maybe Type
Nothing    -> Sort -> Sort -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Term -> Sort
unwrapSort Term
v) (Term -> Sort
unwrapSort Term
u)
        Just Type
t     -> Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t Term
v Term
u
      where
        isOpen :: Bool
isOpen = MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> MetaInstantiation -> Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv
        getArgs :: Term -> Args
getArgs = \case
            Sort (MetaS MetaId
_ Elims
es) -> Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
            MetaV MetaId
_ Elims
es        -> Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
            Term
_                 -> Args
forall a. HasCallStack => a
__IMPOSSIBLE__
        unwrapSort :: Term -> Sort
unwrapSort (Sort Sort
s) = Sort
s
        unwrapSort Term
_        = Sort
forall a. HasCallStack => a
__IMPOSSIBLE__

    niceError :: MetaId -> Term -> TCErr -> TCMT IO ()
niceError MetaId
x Term
u TCErr
err = do
      Term
u <- Term -> TCMT IO Term
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 = (Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
cl) { envCall :: Maybe (Closure Call)
envCall = Maybe (Closure Call)
forall a. Maybe a
Nothing } } }
                   TCErr
_ -> TCErr
err
          telList :: [Dom' Term (ArgName, Type)]
telList = Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
genTel
          names :: [ArgName]
names   = (Dom' Term (ArgName, Type) -> ArgName)
-> [Dom' Term (ArgName, Type)] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName)
-> (Dom' Term (ArgName, Type) -> (ArgName, Type))
-> Dom' Term (ArgName, Type)
-> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom) [Dom' Term (ArgName, Type)]
telList
          late :: [ArgName]
late    = (Dom' Term (ArgName, Type) -> ArgName)
-> [Dom' Term (ArgName, Type)] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst ((ArgName, Type) -> ArgName)
-> (Dom' Term (ArgName, Type) -> (ArgName, Type))
-> Dom' Term (ArgName, Type)
-> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (ArgName, Type)] -> [ArgName])
-> [Dom' Term (ArgName, Type)] -> [ArgName]
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type) -> Bool)
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Any -> Bool
getAny (Any -> Bool)
-> (Dom' Term (ArgName, Type) -> Any)
-> Dom' Term (ArgName, Type)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Any) -> Dom' Term (ArgName, Type) -> Any
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (Bool -> Any
Any (Bool -> Any) -> (MetaId -> Bool) -> MetaId -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x))) [Dom' Term (ArgName, Type)]
telList
          projs :: Elim' Term -> Set ArgName
projs (Proj ProjOrigin
_ QName
q)
            | QName
q QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
genRecFields = [ArgName] -> Set ArgName
forall a. Ord a => [a] -> Set a
Set.fromList ([ArgName] -> Set ArgName) -> [ArgName] -> Set ArgName
forall a b. (a -> b) -> a -> b
$ [Maybe ArgName] -> [ArgName]
forall a. [Maybe a] -> [a]
catMaybes [QName -> Maybe ArgName
getGeneralizedFieldName QName
q]
          projs Elim' Term
_                 = Set ArgName
forall a. Set a
Set.empty
          early :: [ArgName]
early = Set ArgName -> [ArgName]
forall a. Set a -> [a]
Set.toList (Set ArgName -> [ArgName]) -> Set ArgName -> [ArgName]
forall a b. (a -> b) -> a -> b
$ ((Term -> Set ArgName) -> Term -> Set ArgName)
-> Term -> (Term -> Set ArgName) -> Set ArgName
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Term -> Set ArgName) -> Term -> Set ArgName
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term
u ((Term -> Set ArgName) -> Set ArgName)
-> (Term -> Set ArgName) -> Set ArgName
forall a b. (a -> b) -> a -> b
$ \ case
                  Var Int
_ Elims
es   -> (Elim' Term -> Set ArgName) -> Elims -> Set ArgName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set ArgName
projs Elims
es
                  Def QName
_ Elims
es   -> (Elim' Term -> Set ArgName) -> Elims -> Set ArgName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set ArgName
projs Elims
es
                  MetaV MetaId
_ Elims
es -> (Elim' Term -> Set ArgName) -> Elims -> Set ArgName
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set ArgName
projs Elims
es
                  Term
_          -> Set ArgName
forall a. Set a
Set.empty
          commas :: [ArgName] -> ArgName
commas []       = ArgName
forall a. HasCallStack => a
__IMPOSSIBLE__
          commas [ArgName
x]      = ArgName
x
          commas [ArgName
x, ArgName
y]   = ArgName
x ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
", and " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
y
          commas (ArgName
x : [ArgName]
xs) = ArgName
x ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
", " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [ArgName] -> ArgName
commas [ArgName]
xs
          cause :: ArgName
cause = ArgName
"There were unsolved constraints that obscured the " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
                  ArgName
"dependencies between the generalized variables."
          solution :: ArgName
solution = ArgName
"The most reliable solution is to provide enough information to make the dependencies " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
                     ArgName
"clear, but simply mentioning the variables in the right order should also work."
          order :: TCM Doc
order = [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ArgName
"Dependency analysis suggested this (likely incorrect) order:",
                        Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ([ArgName] -> ArgName
unwords [ArgName]
names) ]
          guess :: ArgName
guess = ArgName
"After constraint solving it looks like " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [ArgName] -> ArgName
commas [ArgName]
late ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" actually depend" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
                  ArgName
" on " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [ArgName] -> ArgName
commas [ArgName]
early
            where
              s :: ArgName
s | [ArgName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgName]
late Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = ArgName
"s"
                | Bool
otherwise        = ArgName
""
      Doc -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords (ArgName -> TCM Doc) -> ArgName -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"Variable generalization failed."
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [TCM Doc
"- Probable cause", Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ArgName
cause]
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [TCM Doc
"- Suggestion", Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ArgName
solution]
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc
"- Further information"
                         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
order ] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
                         [ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ArgName
guess | Bool -> Bool
not ([ArgName] -> Bool
forall a. Null a => a -> Bool
null [ArgName]
late), Bool -> Bool
not ([ArgName] -> Bool
forall a. Null a => a -> Bool
null [ArgName]
early) ] [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++
                         [ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
fwords ArgName
"The dependency I error is", TCErr -> TCM Doc
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 =
      t (Dom' t (Name, b))
-> (Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ t (Dom' t (Name, b))
cxt ((Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ())
-> (Dom' t (Name, b) -> TCMT IO ()) -> TCMT IO ()
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!)
        ArgName -> Int -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.generalize.eta.scope" Int
40 (ArgName -> TCMT IO ()) -> ArgName -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgName
"Adding (or not) " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> Name
nameConcrete Name
x) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" to the scope"
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Char
'.' Char -> ArgName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> Name
nameConcrete Name
x)) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
          ArgName -> Int -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.generalize.eta.scope" Int
40 ArgName
"  (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 = [ArgInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgInfo]
infos
    appl :: ArgInfo -> a -> Elim' a
appl ArgInfo
info a
v = Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info a
v)
    recVal :: Term
recVal = ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Term -> Elim' Term) -> [ArgInfo] -> [Term] -> Elims
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArgInfo -> Term -> Elim' Term
forall a. ArgInfo -> a -> Elim' a
appl [ArgInfo]
infos ([Term] -> Elims) -> [Term] -> Elims
forall a b. (a -> b) -> a -> b
$ [Int -> Term
var Int
j | Int
j <- [Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2..Int
0]] [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ Int -> Term -> [Term]
forall a. Int -> a -> [a]
replicate (Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Term
HasCallStack => Term
__DUMMY_TERM__

    -- want: Γ Δᵢ ⊢ recSub i : Γ (r : R)
    -- have:
    -- Γ Δᵢ ⊢ recVal i :# σ : Θ (r : R),  if Γ Δᵢ ⊢ σ : Θ
    -- Γ Δᵢ ⊢ WkS i IdS : Γ
    recSub :: Substitution
recSub = Term
recVal Term -> Substitution -> Substitution
forall a. a -> Substitution' a -> Substitution' a
:# Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
Wk Int
i Substitution
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 ArgName, Type)] -> Telescope
buildGeneralizeTel ConHead
con [(Arg ArgName, Type)]
xs = Int -> [(Arg ArgName, Type)] -> Telescope
go Int
0 [(Arg ArgName, Type)]
xs
  where
    infos :: [ArgInfo]
infos = ((Arg ArgName, Type) -> ArgInfo)
-> [(Arg ArgName, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Arg ArgName -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo (Arg ArgName -> ArgInfo)
-> ((Arg ArgName, Type) -> Arg ArgName)
-> (Arg ArgName, Type)
-> ArgInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg ArgName, Type) -> Arg ArgName
forall a b. (a, b) -> a
fst) [(Arg ArgName, Type)]
xs
    recSub :: Int -> Substitution
recSub Int
i = ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub ConHead
con [ArgInfo]
infos Int
i
    go :: Int -> [(Arg ArgName, Type)] -> Telescope
go Int
_ [] = Telescope
forall a. Tele a
EmptyTel
    go Int
i ((Arg ArgName
name, Type
ty) : [(Arg ArgName, Type)]
xs) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
dom Type
ty') (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs (Arg ArgName -> ArgName
forall e. Arg e -> e
unArg Arg ArgName
name) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [(Arg ArgName, Type)] -> Telescope
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Arg ArgName, Type)]
xs
      where ty' :: Type
ty' = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution
recSub Int
i) Type
ty
            dom :: Type -> Dom Type
dom = ArgInfo -> ArgName -> Type -> Dom Type
forall a. ArgInfo -> ArgName -> a -> Dom a
defaultNamedArgDom (Arg ArgName -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg ArgName
name) (Arg ArgName -> ArgName
forall e. Arg e -> e
unArg Arg ArgName
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 <- Lens' DoGeneralize TCEnv
-> (DoGeneralize -> DoGeneralize)
-> TCMT IO [(QName, MetaId, GeneralizedValue)]
-> TCMT IO [(QName, MetaId, GeneralizedValue)]
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' DoGeneralize TCEnv
eGeneralizeMetas (DoGeneralize -> DoGeneralize -> DoGeneralize
forall a b. a -> b -> a
const DoGeneralize
YesGeneralizeVar) (TCMT IO [(QName, MetaId, GeneralizedValue)]
 -> TCMT IO [(QName, MetaId, GeneralizedValue)])
-> TCMT IO [(QName, MetaId, GeneralizedValue)]
-> TCMT IO [(QName, MetaId, GeneralizedValue)]
forall a b. (a -> b) -> a -> b
$
               (QName -> TCMT IO (QName, MetaId, GeneralizedValue))
-> [QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO (QName, MetaId, GeneralizedValue)
createGenValue ([QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)])
-> [QName] -> TCMT IO [(QName, MetaId, GeneralizedValue)]
forall a b. (a -> b) -> a -> b
$ (QName -> QName -> Ordering) -> [QName] -> [QName]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Range -> Range -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Range -> Ordering)
-> (QName -> Range) -> QName -> QName -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` QName -> Range
forall a. HasRange a => a -> Range
getRange) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
s
  let metaMap :: Map MetaId QName
metaMap = (QName -> QName -> QName) -> [(MetaId, QName)] -> Map MetaId QName
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith QName -> QName -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__ [ (MetaId
m, QName
x) | (QName
x, MetaId
m, GeneralizedValue
_) <- [(QName, MetaId, GeneralizedValue)]
genvals ]
      nameMap :: Map QName GeneralizedValue
nameMap = (GeneralizedValue -> GeneralizedValue -> GeneralizedValue)
-> [(QName, GeneralizedValue)] -> Map QName GeneralizedValue
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith GeneralizedValue -> GeneralizedValue -> GeneralizedValue
forall a. HasCallStack => a
__IMPOSSIBLE__ [ (QName
x, GeneralizedValue
v) | (QName
x, MetaId
_, GeneralizedValue
v) <- [(QName, MetaId, GeneralizedValue)]
genvals ]
  (Map MetaId QName, Map QName GeneralizedValue)
-> TCM (Map MetaId QName, Map QName GeneralizedValue)
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 -> TCMT IO (QName, MetaId, GeneralizedValue)
createGenValue QName
x = QName
-> TCMT IO (QName, MetaId, GeneralizedValue)
-> TCMT IO (QName, MetaId, GeneralizedValue)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (TCMT IO (QName, MetaId, GeneralizedValue)
 -> TCMT IO (QName, MetaId, GeneralizedValue))
-> TCMT IO (QName, MetaId, GeneralizedValue)
-> TCMT IO (QName, MetaId, GeneralizedValue)
forall a b. (a -> b) -> a -> b
$ do
  CheckpointId
cp  <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
  Definition
def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
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 :: p -> p
hideExplicit p
arg | p -> Bool
forall a. LensHiding a => a -> Bool
visible p
arg = p -> p
forall a. LensHiding a => a -> a
hide p
arg
                       | Bool
otherwise   = p
arg
      argTel :: Telescope
argTel     = [Dom' Term (ArgName, Type)] -> Telescope
telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
-> [Dom' Term (ArgName, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type))
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type)
forall a. LensHiding a => a -> a
hideExplicit ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. Int -> [a] -> [a]
take Int
nGen ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel

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

  let name :: ArgName
name     = Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x)
  (MetaId
m, Term
term) <- RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck ArgName
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.
  MetaId -> (MetaVariable -> MetaVariable) -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> TCMT IO ())
-> (MetaVariable -> MetaVariable) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
    Quantity -> MetaVariable -> MetaVariable
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> ArgInfo
defArgInfo Definition
def)) (MetaVariable -> MetaVariable) -> MetaVariable -> MetaVariable
forall a b. (a -> b) -> a -> b
$
    MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }

  -- Set up names of arg metas
  [(Integer, Term, Dom' Term (ArgName, Type))]
-> ((Integer, Term, Dom' Term (ArgName, Type)) -> TCMT IO ())
-> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Integer]
-> [Term]
-> [Dom' Term (ArgName, Type)]
-> [(Integer, Term, Dom' Term (ArgName, Type))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Integer
1..] ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
args) (Telescope -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
argTel)) (((Integer, Term, Dom' Term (ArgName, Type)) -> TCMT IO ())
 -> TCMT IO ())
-> ((Integer, Term, Dom' Term (ArgName, Type)) -> TCMT IO ())
-> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ case
    (Integer
i, MetaV MetaId
m Elims
_, Dom{unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
x, Type
_)}) -> do
      let suf :: ArgName -> ArgName
suf ArgName
"_" = Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
i
          suf ArgName
""  = Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
i
          suf ArgName
x   = ArgName
x
      MetaId -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
m (ArgName
name ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName -> ArgName
suf ArgName
x)
    (Integer, Term, Dom' Term (ArgName, Type))
_ -> () -> TCMT IO ()
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.
  MetaId -> ArgInfo -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m (ArgInfo -> TCMT IO ()) -> ArgInfo -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> ArgInfo
forall a. LensHiding a => a -> a
hideExplicit (Definition -> ArgInfo
defArgInfo Definition
def)

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

  case Term
term of
    MetaV{} -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Term
_       -> Doc -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Doc
"Cannot generalize over" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"of eta-expandable type") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?>
                                    Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
metaType
  (QName, MetaId, GeneralizedValue)
-> TCMT IO (QName, MetaId, GeneralizedValue)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x, MetaId
m, GeneralizedValue :: CheckpointId -> Term -> Type -> GeneralizedValue
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 <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  let freshQName :: ArgName -> TCMT IO QName
freshQName ArgName
s = ModuleName -> Name -> QName
qualify ModuleName
current (Name -> QName) -> TCMT IO Name -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (ArgName
s :: String)
      mkFieldName :: MetaId -> TCMT IO QName
mkFieldName  = ArgName -> TCMT IO QName
freshQName (ArgName -> TCMT IO QName)
-> (ArgName -> ArgName) -> ArgName -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName
generalizedFieldName ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++) (ArgName -> TCMT IO QName)
-> (MetaId -> TCMT IO ArgName) -> MetaId -> TCMT IO QName
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< MetaId -> TCMT IO ArgName
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion
  [Dom QName]
genRecFields <- (MetaId -> TCMT IO (Dom QName)) -> [MetaId] -> TCMT IO [Dom QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QName -> Dom QName
forall a. a -> Dom a
defaultDom (QName -> Dom QName)
-> (MetaId -> TCMT IO QName) -> MetaId -> TCMT IO (Dom QName)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> TCMT IO QName
mkFieldName) [MetaId]
sortedMetas
  QName
genRecName   <- ArgName -> TCMT IO QName
freshQName ArgName
"GeneralizeTel"
  ConHead
genRecCon    <- ArgName -> TCMT IO QName
freshQName ArgName
"mkGeneralizeTel" TCMT IO QName -> (QName -> ConHead) -> TCMT IO ConHead
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ QName
con -> ConHead :: QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead
                  { conName :: QName
conName      = QName
con
                  , conDataRecord :: DataOrRecord
conDataRecord= PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching
                  , conInductive :: Induction
conInductive = Induction
Inductive
                  , conFields :: [Arg QName]
conFields    = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
genRecFields
                  }
  Int
projIx <- Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int)
-> ([Dom (Name, Type)] -> Int) -> [Dom (Name, Type)] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Dom (Name, Type)] -> Int
forall a. Sized a => a -> Int
size ([Dom (Name, Type)] -> Int)
-> TCMT IO [Dom (Name, Type)] -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
  TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [(MetaId, Dom QName)]
-> ((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([MetaId] -> [Dom QName] -> [(MetaId, Dom QName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [MetaId]
sortedMetas [Dom QName]
genRecFields) (((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ())
-> ((MetaId, Dom QName) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (MetaId
meta, Dom QName
fld) -> do
    Type
fieldTy <- MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
meta
    let field :: QName
field = Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
fld
    QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
field (Dom QName -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom QName
fld) QName
field Type
fieldTy (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      let proj :: Projection
proj = Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
Projection { projProper :: Maybe QName
projProper   = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
genRecName
                            , projOrig :: QName
projOrig     = QName
field
                            , projFromType :: Arg QName
projFromType = QName -> Arg QName
forall a. a -> Arg a
defaultArg QName
genRecName
                            , projIndex :: Int
projIndex    = Int
projIx
                            , projLams :: ProjLams
projLams     = [Arg ArgName] -> ProjLams
ProjLams [ArgName -> Arg ArgName
forall a. a -> Arg a
defaultArg ArgName
"gtel"] } in
      Function :: [Clause]
-> Maybe CompiledClauses
-> Maybe SplitTree
-> Maybe Compiled
-> [Clause]
-> FunctionInverse
-> Maybe [QName]
-> IsAbstract
-> Delayed
-> Maybe Projection
-> Set FunctionFlag
-> Maybe Bool
-> Maybe ExtLamInfo
-> Maybe QName
-> Defn
Function { funClauses :: [Clause]
funClauses      = []
               , funCompiled :: Maybe CompiledClauses
funCompiled     = Maybe CompiledClauses
forall a. Maybe a
Nothing
               , funSplitTree :: Maybe SplitTree
funSplitTree    = Maybe SplitTree
forall a. Maybe a
Nothing
               , funTreeless :: Maybe Compiled
funTreeless     = Maybe Compiled
forall a. Maybe a
Nothing
               , funInv :: FunctionInverse
funInv          = FunctionInverse
forall c. FunctionInverse' c
NotInjective
               , funMutual :: Maybe [QName]
funMutual       = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
               , funAbstr :: IsAbstract
funAbstr        = IsAbstract
ConcreteDef
               , funDelayed :: Delayed
funDelayed      = Delayed
NotDelayed
               , funProjection :: Maybe Projection
funProjection   = Projection -> Maybe Projection
forall a. a -> Maybe a
Just Projection
proj
               , funFlags :: Set FunctionFlag
funFlags        = Set FunctionFlag
forall a. Set a
Set.empty
               , funTerminates :: Maybe Bool
funTerminates   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
               , funExtLam :: Maybe ExtLamInfo
funExtLam       = Maybe ExtLamInfo
forall a. Maybe a
Nothing
               , funWith :: Maybe QName
funWith         = Maybe QName
forall a. Maybe a
Nothing
               , funCovering :: [Clause]
funCovering     = []
               }
  QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' (ConHead -> QName
conName ConHead
genRecCon) ArgInfo
defaultArgInfo (ConHead -> QName
conName ConHead
genRecCon) Type
HasCallStack => Type
__DUMMY_TYPE__ (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ -- Filled in later
    Constructor :: Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor { conPars :: Int
conPars   = Int
0
                , conArity :: Int
conArity  = [Dom QName] -> Int
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   = Maybe [QName]
forall a. Maybe a
Nothing
                , conForced :: [IsForced]
conForced = []
                , conErased :: Maybe [Bool]
conErased = Maybe [Bool]
forall a. Maybe a
Nothing
                }
  let dummyTel :: t -> Telescope
dummyTel t
0 = Telescope
forall a. Tele a
EmptyTel
      dummyTel t
n = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
HasCallStack => Type
__DUMMY_TYPE__) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs ArgName
"_" (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ t -> Telescope
dummyTel (t
n t -> t -> t
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) (Defn -> TCMT IO ()) -> Defn -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    Record :: Int
-> Maybe Clause
-> ConHead
-> Bool
-> [Dom QName]
-> Telescope
-> Maybe [QName]
-> EtaEquality
-> PatternOrCopattern
-> Maybe Induction
-> IsAbstract
-> CompKit
-> Defn
Record { recPars :: Int
recPars         = Int
0
           , recClause :: Maybe Clause
recClause       = Maybe Clause
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          = Int -> Telescope
forall t. (Eq t, Num t) => t -> Telescope
dummyTel ([Dom QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
genRecFields) -- Filled in later
           , recMutual :: Maybe [QName]
recMutual       = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
           , recEtaEquality' :: EtaEquality
recEtaEquality' = HasEta -> EtaEquality
Inferred HasEta
forall a. HasEta' a
YesEta
           , recPatternMatching :: PatternOrCopattern
recPatternMatching = PatternOrCopattern
CopatternMatching
           , recInduction :: Maybe Induction
recInduction    = Maybe Induction
forall a. Maybe a
Nothing
           , recAbstr :: IsAbstract
recAbstr        = IsAbstract
ConcreteDef
           , recComp :: CompKit
recComp         = CompKit
emptyCompKit
           }
  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"created genRec" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Dom QName -> TCM Doc) -> [Dom QName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc)
-> (Dom QName -> ArgName) -> Dom QName -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (QName -> ArgName) -> (Dom QName -> QName) -> Dom QName -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
genRecFields) ]
  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
80 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"created genRec" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ([Dom QName] -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow [Dom QName]
genRecFields) ]
  -- Solve the genRecMeta
  Args
args <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let genRecTy :: Type
genRecTy = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
genRecSort (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
genRecName (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args
  TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
genRecTy Type
genRecMeta
  (QName, ConHead, [QName]) -> TCMT IO (QName, ConHead, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
genRecName, ConHead
genRecCon, (Dom QName -> QName) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> QName
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 <- (Dom Type -> Dom Type) -> Telescope -> Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dom Type -> Dom Type
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  let fullTel :: Telescope
fullTel = Telescope
cxtTel Telescope -> Telescope -> Telescope
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) =
          Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
cxtTel (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
recTy) (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
"r" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
ty)) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:
          [QName] -> Telescope -> [Type]
mkFieldTypes [QName]
flds (Abs Telescope -> SubstArg Telescope -> Telescope
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
ftel Term
SubstArg Telescope
proj)
        where
          s :: Sort
s = Dom Type -> Abs Type -> Sort
mkPiSort (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
recTy) (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
"r" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
ty)
          proj :: Term
proj = Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fld]
      mkFieldTypes [QName]
_ Telescope
_ = [Type]
forall a. HasCallStack => a
__IMPOSSIBLE__
  let fieldTypes :: [Type]
fieldTypes = [QName] -> Telescope -> [Type]
mkFieldTypes [QName]
fields (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
1 Telescope
fieldTel)
  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Field types:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Type -> TCM Doc) -> [Type] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
fieldTypes)
  (QName -> Type -> TCMT IO ()) -> [QName] -> [Type] -> TCMT IO ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ QName -> Type -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => QName -> Type -> m ()
setType [QName]
fields [Type]
fieldTypes
  -- Constructor type
  let conType :: Type
conType = Telescope
fullTel Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
`abstract` Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
fieldTel) Type
recTy
  ArgName -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.generalize" Int
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text ArgName
"Final genRecCon type:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
conType)
  QName -> Type -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => QName -> Type -> m ()
setType (ConHead -> QName
conName ConHead
con) Type
conType
  -- Record telescope: Includes both parameters and fields.
  QName -> (Definition -> Definition) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
name ((Definition -> Definition) -> TCMT IO ())
-> (Definition -> Definition) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ Definition
r ->
    Definition
r { theDef :: Defn
theDef = (Definition -> Defn
theDef Definition
r) { recTel :: Telescope
recTel = Telescope
fullTel } }
  where
    setType :: QName -> Type -> m ()
setType QName
q Type
ty = QName -> (Definition -> Definition) -> m ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q ((Definition -> Definition) -> m ())
-> (Definition -> Definition) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Definition
d -> Definition
d { defType :: Type
defType = Type
ty }