{-# OPTIONS_GHC -Wunused-imports #-}

{-|

This module implements the type checking part of generalisable variables. When we get here we have
a type checking problem for a type (or telescope) containing a known set of generalisable variables
and we need to produce a well typed type (or telescope) with the correct generalisations. For instance,
given

@
variable
  A  : Set
  n  : Nat
  xs : Vec A n

foo : SomeType xs
@

generalisation should produce @{A : Set} {n : Nat} {xs : Vec A n} → SomeType xs@ for the type of
@foo@.

The functions 'generalizeType' and 'generalizeTelescope' don't have access to the abstract syntax to
be type checked (@SomeType xs@ in the example). Instead they are provided a type checking action
that delivers a 'Type' or a 'Telescope'. The challenge is setting up a context in which @SomeType
xs@ can be type checked successfully by this action, without knowing what the telescope of
generalised variables will be. Once we have computed this telescope the result needs to be
transformed into a well typed type abstracted over it.

__At no point are we allowed to cheat!__ Any transformation between well typed terms needs to be done
by well typed substitutions.

The key idea is to run the type checking action in the context of a single variable of an unknown
type. Once we know what variables to generalise over this type is instantiated to a fresh record
type with a field for each generalised variable. Turning the result of action into something valid
in the context of the generalised variables is then a simple substitution unpacking the record
variable.

In more detail, generalisation proceeds as follows:

- Add a variable @genTel@ of an unknown type to the context ('withGenRecVar').

@
  (genTel : _GenTel)
@

- Create metavariables for the generalisable variables appearing in the problem and their
  dependencies ('createGenValues'). In the example this would be

@
  (genTel : _GenTel) ⊢
    _A  : Set
    _n  : Nat
    _xs : Vec _A _n
@

- Run the type checking action ('createMetasAndTypeCheck'), binding the mentioned generalisable
  variables to the corresponding newly created metavariables. This binding is stored in
  'eGeneralizedVars' and picked up in 'Agda.TypeChecking.Rules.Application.inferDef'

@
  (genTel : _GenTel) ⊢ SomeType (_xs genTel)
@

- Compute the telescope of generalised variables ('computeGeneralization'). This is done by taking
  the unconstrained metavariables created by 'createGenValues' or created during the type checking
  action and sorting them into a well formed telescope.

@
  {A : Set} {n : Nat} {xs : Vec A n}
@

- Create a record type @GeneralizeTel@ whose fields are the generalised variables and instantiate
  the type of @genTel@ to it ('createGenRecordType').

@
  record GeneralizeTel : Set₁ where
    constructor mkGeneralizeTel
    field
      A  : Set
      n  : Nat
      xs : Vec A n
@

- Solve the metavariables with their corresponding projections from @genTel@.

@
  _A  := λ genTel → genTel .A
  _n  := λ genTel → genTel .n
  _xs := λ genTel → genTel .xs
@

- Build the unpacking substitution ('unpackSub') that maps terms in @(genTel : GeneralizeTel)@ to
  terms in the context of the generalised variables by substituting a record value for @genTel@.

@
  {A : Set} {n : Nat} {xs : Vec A n} ⊢ [mkGeneralizeTel A n xs / genTel] : (genTel : GeneralizeTel)
@

- Build the final result by applying the unpacking substitution to the result of the type checking
  action and abstracting over the generalised telescope.

@
  {A : Set} {n : Nat} {xs : Vec A n} → SomeType (_xs (mkGeneralizeTel A n xs)) ==
  {A : Set} {n : Nat} {xs : Vec A n} → SomeType xs
@

- In case of 'generalizeType' return the resulting pi type.
- In case of 'generalizeTelescope' enter the resulting context, applying the unpacking substitution
  to let bindings (TODO #6916: and also module applications!) created in the telescope, and call the
  continuation.

-}

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

import Prelude hiding (null)

import Control.Monad.Except ( MonadError(..) )

import Data.Set (Set)
import Data.Set qualified as Set
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.HashMap.Strict qualified as HMap
import Data.List (partition, sortBy)
import Data.Monoid

import Agda.Interaction.Options.Base

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow, singPlural)
import Agda.Syntax.Concrete.Name (LensInScope(..))
import Agda.Syntax.Position
import Agda.Syntax.Info          (MetaNameSuggestion)
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.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.Function
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Set1 as Set1
import Agda.Utils.Size
import Agda.Utils.Permutation
import qualified Agda.Utils.VarSet as VarSet

-- | Generalize a telescope over a set of generalizable variables.
generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
generalizeTelescope :: forall a.
Map QName Name
-> (forall a. (Tele (Dom Type) -> TCM a) -> TCM a)
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars forall a. (Tele (Dom Type) -> TCM a) -> TCM a
typecheckAction [Maybe Name] -> Tele (Dom Type) -> TCM a
ret | Map QName Name -> Bool
forall k a. Map k a -> Bool
Map.null Map QName Name
vars = (Tele (Dom Type) -> TCM a) -> TCM a
forall a. (Tele (Dom Type) -> TCM a) -> TCM a
typecheckAction ([Maybe Name] -> Tele (Dom Type) -> TCM a
ret [])
generalizeTelescope Map QName Name
vars forall a. (Tele (Dom Type) -> TCM a) -> TCM a
typecheckAction [Maybe Name] -> Tele (Dom Type) -> 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
  sectionsBefore <- Lens' TCState (Map ModuleName Section)
-> TCMT IO (Map ModuleName Section)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Map ModuleName Section -> f (Map ModuleName Section))
    -> Signature -> f Signature)
-> (Map ModuleName Section -> f (Map ModuleName Section))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ModuleName Section -> f (Map ModuleName Section))
-> Signature -> f Signature
Lens' Signature (Map ModuleName Section)
sigSections)
  definitionsBefore <- useTC (stSignature . sigDefinitions)
  anonymousModulesBefore <- viewTC eAnonymousModules
  let s = Map QName Name -> Set QName
forall k a. Map k a -> Set k
Map.keysSet Map QName Name
vars
  ((cxtNames, tel, letbinds, anonymousModules), namedMetas, allmetas) <-
    createMetasAndTypeCheck s $ typecheckAction $ \ Tele (Dom Type)
tel -> do
      xs <- Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take' (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) ([Name] -> [Name]) -> TCMT IO [Name] -> TCMT IO [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Name]
forall (m :: * -> *). MonadTCEnv m => m [Name]
getContextNames'
      lbs <- getLetBindings -- This gives let-bindings valid in the current context
      anons <- viewTC eAnonymousModules
      return (xs, tel, lbs, anons)
  sectionsAfter <- useTC (stSignature . sigSections)
  definitionsAfter <- useTC (stSignature . sigDefinitions)
  let newSections = Map ModuleName Section -> Set ModuleName
forall k a. Map k a -> Set k
Map.keysSet (Map ModuleName Section -> Set ModuleName)
-> Map ModuleName Section -> Set ModuleName
forall a b. (a -> b) -> a -> b
$ Map ModuleName Section
-> Map ModuleName Section -> Map ModuleName Section
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map ModuleName Section
sectionsAfter Map ModuleName Section
sectionsBefore
      sectionDefs = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList
        [ QName
q
        | QName
q <- HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
definitionsAfter
        , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> HashMap QName Definition -> Bool
forall k a. Hashable k => k -> HashMap k a -> Bool
HMap.member QName
q HashMap QName Definition
definitionsBefore
        , ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (QName -> ModuleName
qnameModule QName
q) Set ModuleName
newSections
        ]
      newAnonymousModules = Int -> [(ModuleName, Int)] -> [(ModuleName, Int)]
forall a. Int -> [a] -> [a]
take' ([(ModuleName, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ModuleName, Int)]
anonymousModules Int -> Int -> Int
forall a. Num a => a -> a -> a
- [(ModuleName, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ModuleName, Int)]
anonymousModulesBefore) [(ModuleName, Int)]
anonymousModules

  reportSDoc "tc.generalize.metas" 60 $ vcat
    [ "open metas =" <+> (text . show . fmap ((miNameSuggestion &&& miGeneralizable) . mvInfo)) (openMetas $ allmetas)
    ]
  -- Translate the QName to the corresponding bound variable
  (genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas

  let 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 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 a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) QName -> Name
boundVar [Maybe QName]
genTelNames

  tel' <- applySubst sub <$> instantiateFull 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 cxtEntry (Maybe Name
mname, Dom' Term (a, Type)
dom) = do
          let s :: a
s = (a, Type) -> a
forall a b. (a, b) -> a
fst ((a, Type) -> a) -> (a, Type) -> a
forall a b. (a -> b) -> a -> b
$ Dom' Term (a, Type) -> (a, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (a, Type)
dom
          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
<$> a -> m Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => a -> m Name
freshName_ a
s) Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
mname
          return $ CtxVar name (snd <$> dom)
      dropCxt Impossible
err = Substitution' Term -> (Context -> Context) -> m a -> m a
forall a. Substitution' Term -> (Context -> Context) -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution' Term -> (Context -> Context) -> m a -> m a
updateContext (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
err Int
1) (Int -> Context -> Context
cxDrop Int
1)
  genTelCxt <- dropCxt __IMPOSSIBLE__ $ mapM cxtEntry $ reverse $ zip' genTelVars $ telToList genTel

  -- For the explicit module telescope we get the names from the typecheck
  -- action.
  let newTelCxt :: [ContextEntry]
      newTelCxt = (Name -> Dom Type -> ContextEntry)
-> [Name] -> [Dom Type] -> [ContextEntry]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Name -> Dom Type -> ContextEntry
CtxVar [Name]
cxtNames ([Dom Type] -> [ContextEntry]) -> [Dom Type] -> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ [Dom Type] -> [Dom Type]
forall a. [a] -> [a]
reverse ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ (Dom' Term ([Char], Type) -> Dom Type)
-> [Dom' Term ([Char], Type)] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map' ((([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> Type
forall a b. (a, b) -> b
snd) ([Dom' Term ([Char], Type)] -> [Dom Type])
-> [Dom' Term ([Char], Type)] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
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 |Θ| ρ)
  letbinds' <- applySubst (liftS (size tel) sub) <$> instantiateFull letbinds
  -- And sections created by module applications in the telescope (#6916)
  --   Γ (r : R) ⊢ Σ            Σ = sectionApps
  --   Γ Δ       ⊢ Σρ
  forM_ newSections \ ModuleName
m -> do
    sec <- Section -> Maybe Section -> Section
forall a. a -> Maybe a -> a
fromMaybe Section
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Section -> Section)
-> TCMT IO (Maybe Section) -> TCMT IO Section
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO (Maybe Section)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe Section)
getSection ModuleName
m
    tel <- applySubst sub <$> instantiateFull (sec ^. secTelescope)
    modifySignature $ over sigSections $ Map.adjust (set secTelescope tel) m
      -- TODO: do we need to update the module checkpoint for m
  forM_ sectionDefs \ QName
q -> do
    t <- Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
sub (Type -> Type) -> TCMT IO Type -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCMT IO Type)
-> (Definition -> Type) -> Definition -> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCMT IO Type) -> TCMT IO Definition -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q
    modifySignature $ updateDefinition q $ updateDefType $ const t

  let addLet (Name
x, LetBinding IsAxiom
isAxiom Origin
o Term
v Dom Type
dom) = IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
forall a.
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
IsAxiom -> Origin -> Name -> Term -> Dom Type -> m a -> m a
addLetBinding' IsAxiom
isAxiom Origin
o Name
x Term
v Dom Type
dom
  updateContext sub (cxPrepend genTelCxt . cxDrop 1) $
    updateContext (raiseS (size tel')) (cxPrepend newTelCxt) $
      flip (foldr $ uncurry withAnonymousModule) newAnonymousModules $
      flip (foldr addLet) letbinds' $
      ret genTelVars $ abstract genTel tel'

-- | Generalize a type over a set of (used) generalizable variables.
generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType :: Set QName -> TCMT IO Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s TCMT IO Type
typecheckAction = do
  (ns, 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, ())) -> TCMT IO Type -> TCM (Type, ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Type
typecheckAction
  return (ns, t)

-- | Allow returning additional information from the type checking action.
generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' :: forall a.
Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' Set QName
s TCM (Type, a)
typecheckAction = Account (BenchPhase (TCMT IO))
-> TCMT IO ([Maybe QName], Type, a)
-> TCMT IO ([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] (TCMT IO ([Maybe QName], Type, a)
 -> TCMT IO ([Maybe QName], Type, a))
-> TCMT IO ([Maybe QName], Type, a)
-> TCMT IO ([Maybe QName], Type, a)
forall a b. (a -> b) -> a -> b
$ (Type -> TCMT IO ([Maybe QName], Type, a))
-> TCMT IO ([Maybe QName], Type, a)
forall a. (Type -> TCM a) -> TCM a
withGenRecVar ((Type -> TCMT IO ([Maybe QName], Type, a))
 -> TCMT IO ([Maybe QName], Type, a))
-> (Type -> TCMT IO ([Maybe QName], Type, a))
-> TCMT IO ([Maybe QName], Type, a)
forall a b. (a -> b) -> a -> b
$ \ Type
genRecMeta -> do

  ((t, userdata), namedMetas, allmetas) <- Set QName
-> TCM (Type, a)
-> TCM ((Type, a), Map MetaId QName, LocalMetaStores)
forall a.
Set QName -> TCM a -> TCM (a, Map MetaId QName, LocalMetaStores)
createMetasAndTypeCheck Set QName
s TCM (Type, a)
typecheckAction

  reportSDoc "tc.generalize.metas" 60 $ vcat
    [ "open metas =" <+> (text . show . fmap ((miNameSuggestion &&& miGeneralizable) . mvInfo)) (openMetas $ allmetas)
    ]

  (genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas

  t' <- abstract genTel . applySubst sub <$> instantiateFull t

  reportSDoc "tc.generalize" 40 $ vcat
    [ "generalized"
    , nest 2 $ "t =" <+> escapeContext impossible 1 (prettyTCM t') ]

  return (genTelNames, t', userdata)

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

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

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

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

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

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

  cs <- (++) <$> useTC stAwakeConstraints
             <*> useTC stSleepingConstraints

  reportSDoc "tc.generalize" 50 $ "current constraints:" <?> vcat (map' prettyTCM cs)

  constrainedMetas <- Set.unions <$> mapM (constraintMetas . clValue . theConstraint) cs

  reportSDoc "tc.generalize" 30 $ nest 2 $
    "constrainedMetas     = " <+> prettyList_ (map' prettyTCM $ Set.toList constrainedMetas)

  let 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
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 = 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 = 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 (generalizable, nongeneralizable)         = partition isGeneralizable mvs
      (generalizableOpen', generalizableClosed) = partition isOpen generalizable
      (openSortMetas, generalizableOpen)        = partition isSort generalizableOpen'
      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

  reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
    [ "generalizable        = " <+> prettyList_ (map' (prettyTCM . fst) generalizable)
    , "generalizableOpen    = " <+> prettyList_ (map' (prettyTCM . fst) generalizableOpen)
    , "openSortMetas        = " <+> prettyList_ (map' (prettyTCM . fst) openSortMetas)
    ]

  -- Issue 3301: We can't generalize over sorts
  List1.unlessNull openSortMetas $ \ List1 (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
$ Set1 MetaId -> Warning
CantGeneralizeOverSorts (Set1 MetaId -> Warning) -> Set1 MetaId -> Warning
forall a b. (a -> b) -> a -> b
$ NonEmpty MetaId -> Set1 MetaId
forall a. Ord a => NonEmpty a -> NESet a
Set1.fromList (NonEmpty MetaId -> Set1 MetaId) -> NonEmpty MetaId -> Set1 MetaId
forall a b. (a -> b) -> a -> b
$ ((MetaId, MetaVariable) -> MetaId)
-> List1 (MetaId, MetaVariable) -> NonEmpty MetaId
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaId, MetaVariable) -> MetaId
forall a b. (a, b) -> a
fst List1 (MetaId, MetaVariable)
ms

  -- Any meta in the solution of a generalizable meta should be generalized over (if possible).
  cp <- viewTC eCurrentCheckpoint
  let canGeneralize MetaId
x | MetaId -> Bool
isConstrained MetaId
x = Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      canGeneralize MetaId
x = do
          mv   <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
          msub <- enterClosure mv $ \ Range' SrcFile
_ ->
                    CheckpointId -> TCMT IO (Maybe (Substitution' Term))
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Maybe (Substitution' Term))
checkpointSubstitution' CheckpointId
cp
          let 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' Term)
msub, MetaVariable -> Permutation
mvPermutation MetaVariable
mv) of
                  (Just Substitution' Term
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' Term
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' Term), Permutation)
_                            -> Bool
False
          unless sameContext $ reportSDoc "tc.generalize" 20 $ do
            ty <- getMetaType x
            let Perm m xs = mvPermutation mv
            vcat
              [ text "Don't know how to generalize over"
              , nest 2 $ prettyTCM x <+> text ":" <+> prettyTCM ty
              , text "in context"
              , nest 2 $ inTopContext . prettyTCM =<< getContextTelescope
              , text "permutation:" <+> text (show (m, xs))
              , text "subst:" <+> pretty msub ]
          return sameContext

  inherited :: Set MetaId <- Set.unions <$> forM generalizableClosed \ (MetaId
x, MetaVariable
mv) ->
    case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
      InstV Instantiation
inst -> do
        parentName <- MetaId -> TCMT IO [Char]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion MetaId
x
        metas <- filterM canGeneralize . Set.toList .
                 allMetas Set.singleton =<<
                 instantiateFull (instBody inst)
        unless (null metas) do
          reportSDoc "tc.generalize" 40 $
            hcat ["Inherited metas from ", prettyTCM x, ":"] <?> prettyList_ (map' prettyTCM metas)
          -- #4291: Override existing meta name suggestion.
          -- Don't suggest names for explicitly named generalizable metas.
          case filter (`Map.notMember` nameMap) metas of
            -- If we solved the parent with a new meta use the parent name for that.
            [MetaId
m] | MetaV{} <- Instantiation -> Term
instBody Instantiation
inst -> MetaId -> [Char] -> TCMT IO ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
m [Char]
parentName
            -- Otherwise suffix with a number.
            [MetaId]
ms -> (Integer -> MetaId -> TCMT IO ())
-> [Integer] -> [MetaId] -> TCMT IO ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\ Integer
i MetaId
m -> MetaId -> [Char] -> TCMT IO ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
m ([Char]
parentName [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
"." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i)) [Integer
1..] [MetaId]
ms
        return $ Set.fromList metas
      MetaInstantiation
_ -> TCMT IO (Set MetaId)
forall a. HasCallStack => a
__IMPOSSIBLE__

  let (alsoGeneralize, reallyDontGeneralize) = partition (`Set.member` inherited) $ map' fst nongeneralizableOpen
      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]
generalizeOver [MetaId] -> MetaId -> Bool
forall a. Ord a => [a] -> a -> Bool
`hasElem`)

  reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
    [ "alsoGeneralize       = " <+> prettyList_ (map' prettyTCM alsoGeneralize)
    , "reallyDontGeneralize = " <+> prettyList_ (map' prettyTCM reallyDontGeneralize)
    ]

  reportSDoc "tc.generalize" 10 $ "we're generalizing over" <+> prettyList_ (map' prettyTCM 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).
  allSortedMetas <- fromMaybeM (typeError GeneralizeCyclicDependency) $
    dependencySortMetas (generalizeOver ++! reallyDontGeneralize ++! map' fst openSortMetas)
  let sortedMetas = (MetaId -> Bool) -> [MetaId] -> [MetaId]
forall a. (a -> Bool) -> [a] -> [a]
filter MetaId -> Bool
shouldGeneralize [MetaId]
allSortedMetas

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

  -- Create the pre-record type (we don't yet know the types of the fields)
  (genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
      createGenRecordType genRecMeta sortedMetas

  reportSDoc "tc.generalize" 30 $ vcat $
    [ "created genRecordType"
    , nest 2 $ "genRecName   = " <+> prettyTCM genRecName
    , nest 2 $ "genRecCon    = " <+> prettyTCM genRecCon
    , nest 2 $ "genRecFields = " <+> prettyList_ (map' prettyTCM genRecFields)
    ]

  -- Solve the generalizable metas. Each generalizable meta is solved by projecting the
  -- corresponding field from the genTel record.
  cxtTel <- getContextTelescope
  let solve MetaId
m QName
field = do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.generalize" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"solving generalized meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> 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, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isInstantiatedMeta MetaId
m) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        MetaId -> [Arg [Char]] -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
m (Tele (Dom Type) -> [Arg [Char]]
forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom Type)
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]
  zipWithM_ solve sortedMetas genRecFields

  -- Record the named variables in the telescope
  let 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
  teleTypes <- do
    args <- getContextArgs
    concat <$> forM sortedMetas \ MetaId
m -> do
      mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      let 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) { argInfoOrigin = Generalization }
          HasType{ jMetaType = t } = mvJudgement mv
          perm = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
      t' <- piApplyM t $ permute (takeP (length args) perm) args
      return [(Arg info $ miNameSuggestion $ mvInfo mv, t')]
  let genTel = ConHead -> [(Arg [Char], Type)] -> Tele (Dom Type)
buildGeneralizeTel ConHead
genRecCon [(Arg [Char], Type)]
teleTypes

  reportSDoc "tc.generalize" 40 $ vcat
    [ text "teleTypes =" <+> prettyTCM teleTypes
    , text "genTel    =" <+> prettyTCM 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
ii, InteractionPoint{ipMeta :: InteractionPoint -> Maybe MetaId
ipMeta = Just MetaId
x})
        | MetaId -> Map MetaId MetaVariable -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member MetaId
x (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
allmetas) Bool -> Bool -> Bool
||
          MetaId -> Map MetaId MetaVariable -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member MetaId
x (LocalMetaStores -> Map MetaId MetaVariable
solvedMetas LocalMetaStores
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
  ips <- Map.fromDistinctAscList . mapMaybe inscope . fst . BiMap.toDistinctAscendingLists <$> useTC stInteractionPoints
  pruneUnsolvedMetas genRecName genRecCon genTel genRecFields ips shouldGeneralize allSortedMetas

  -- Fill in the missing details of the telescope record.
  dropCxt __IMPOSSIBLE__ $ fillInGenRecordDetails genRecName genRecCon genRecFields genRecMeta 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 = ConHead -> [ArgInfo] -> Int -> Substitution' Term
unpackSub ConHead
genRecCon (((Arg [Char], Type) -> ArgInfo)
-> [(Arg [Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg [Char] -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo (Arg [Char] -> ArgInfo)
-> ((Arg [Char], Type) -> Arg [Char])
-> (Arg [Char], Type)
-> ArgInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg [Char], Type) -> Arg [Char]
forall a b. (a, b) -> a
fst) [(Arg [Char], Type)]
teleTypes) ([(Arg [Char], Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Arg [Char], Type)]
teleTypes)

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

  return (genTel, telNames, 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
-> Tele (Dom Type)
-> [QName]
-> Map MetaId InteractionId
-> (MetaId -> Bool)
-> [MetaId]
-> TCMT IO ()
pruneUnsolvedMetas QName
genRecName ConHead
genRecCon Tele (Dom Type)
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise               = [Dom' Term ([Char], Type)]
-> Tele (Dom Type) -> [MetaId] -> TCMT IO ()
prune [] Tele (Dom Type)
genTel [MetaId]
metas
  where
    prune :: ListTel -> Telescope -> [MetaId] -> TCM ()
    prune :: [Dom' Term ([Char], Type)]
-> Tele (Dom Type) -> [MetaId] -> TCMT IO ()
prune [Dom' Term ([Char], Type)]
_ Tele (Dom Type)
_ [] = () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    prune [Dom' Term ([Char], Type)]
cxt Tele (Dom Type)
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
        x <- if Tele (Dom Type) -> Bool
forall a. Null a => a -> Bool
null Tele (Dom Type)
tel then MetaId -> TCMT IO MetaId
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x else MetaId -> TCMT IO MetaId
prePrune MetaId
x
        pruneMeta (telFromList $ reverse cxt) x
      [Dom' Term ([Char], Type)]
-> Tele (Dom Type) -> [MetaId] -> TCMT IO ()
prune [Dom' Term ([Char], Type)]
cxt Tele (Dom Type)
tel [MetaId]
xs
    prune [Dom' Term ([Char], Type)]
cxt (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) (MetaId
x : [MetaId]
xs) = [Dom' Term ([Char], Type)]
-> Tele (Dom Type) -> [MetaId] -> TCMT IO ()
prune ((Type -> ([Char], Type)) -> Dom Type -> Dom' Term ([Char], Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char]
x,) Dom Type
a Dom' Term ([Char], Type)
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. a -> [a] -> [a]
: [Dom' Term ([Char], Type)]
cxt) (Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Abs a -> a
unAbs Abs (Tele (Dom Type))
tel) [MetaId]
xs
      where x :: [Char]
x = Abs (Tele (Dom Type)) -> [Char]
forall a. Abs a -> [Char]
absName Abs (Tele (Dom Type))
tel
    prune [Dom' Term ([Char], Type)]
_ Tele (Dom Type)
_ [MetaId]
_ = TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

    -- 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 -> TCM MetaId
    prePrune :: MetaId -> TCMT IO MetaId
prePrune MetaId
x = do
      cp <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
      mv <- lookupLocalMeta x
      (i, _A) <- enterClosure mv $ \ Range' SrcFile
_ -> do
        δ <- CheckpointId -> TCMT IO (Substitution' Term)
forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Substitution' Term)
checkpointSubstitution CheckpointId
cp
        _A <- case mvJudgement mv of
                IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
forall a. a -> TCMT IO a
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) -> TCMT IO Type -> TCMT IO (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
x
        case δ of
          Wk Int
n Substitution' Term
IdS -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, Maybe Type
_A)
          Substitution' Term
IdS      -> (Int, Maybe Type) -> TCMT IO (Int, Maybe Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
0, Maybe Type
_A)
          Substitution' Term
_        -> TypeError -> TCMT IO (Int, Maybe Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Int, Maybe Type))
-> (Closure MetaId -> TypeError)
-> Closure MetaId
-> TCMT IO (Int, Maybe Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure MetaId -> TypeError
GeneralizationPrepruneErrorRefinedContext (Closure MetaId -> TCMT IO (Int, Maybe Type))
-> TCMT IO (Closure MetaId) -> TCMT IO (Int, Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO (Closure MetaId)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure MetaId
x
      if i == 0 then return x else do
        reportSDoc "tc.generalize.prune.pre" 40 $ vcat
          [ "prepruning"
          , nest 2 $ pretty x <+> ":" <+> pretty (jMetaType $ mvJudgement mv)
          , nest 2 $ "|Δ| =" <+> pshow 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 VarSet.minView (freeVarSet _A) of
          Just (Int
j, VarSet
_) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Closure MetaId -> TypeError) -> Closure MetaId -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure MetaId -> TypeError
GeneralizationPrepruneErrorCyclicDependencies (Closure MetaId -> TCMT IO ())
-> TCMT IO (Closure MetaId) -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO (Closure MetaId)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure MetaId
x
          Maybe (Int, VarSet)
_                   -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

        (y, u) <- newMetaFromOld mv ρ _A

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

        reportSDoc "tc.generalize.prune.pre" 40 $ nest 2 $ vcat
          [ "u    =" <+> pretty u
          , "uρ⁻¹ =" <+> pretty uρ' ]

        -- To solve it we enter the context of x again
        enterClosure mv $ \ Range' SrcFile
_ -> do
          -- v is x applied to the context variables
          v <- case Maybe Type
_A of
                 Maybe Type
Nothing -> Sort -> Term
Sort (Sort -> Term) -> ([Arg Term] -> Sort) -> [Arg Term] -> 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) -> ([Arg Term] -> Elims) -> [Arg Term] -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> TCMT IO [Arg Term] -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m [Arg Term]
getMetaContextArgs MetaVariable
mv
                 Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> TCMT IO [Arg Term] -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m [Arg Term]
getMetaContextArgs MetaVariable
mv
          noConstraints (doPrune x mv _A v uρ') `catchError` \ TCErr
_ ->
            TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Closure MetaId -> TypeError) -> Closure MetaId -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure MetaId -> TypeError
GeneralizationPrepruneErrorFailedToInstantiate (Closure MetaId -> TCMT IO ())
-> TCMT IO (Closure MetaId) -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO (Closure MetaId)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure MetaId
x
          setInteractionPoint x y
          return y

    pruneMeta :: Telescope -> MetaId -> TCM ()
    pruneMeta :: Tele (Dom Type) -> MetaId -> TCMT IO ()
pruneMeta Tele (Dom Type)
_Θ MetaId
x = do
      cp <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
      mv <- lookupLocalMeta 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.
      enterClosure mv $ \ Range' SrcFile
_ ->
        -- 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

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

        _ΓrΔ <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope
        let (_Γ, _Δ) = (telFromList gs, telFromList ds)
              where (gs, _ : ds) = splitAt (size _ΓrΔ - i - 1) (telToList _ΓrΔ)

        -- Get the type of x. By doing this here we let the checkpoint machinery sort out the
        _A <- case mvJudgement mv of
                IsSort{}  -> Maybe Type -> TCMT IO (Maybe Type)
forall a. a -> TCMT IO a
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) -> TCMT IO Type -> TCMT IO (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce 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)
        δ <- checkpointSubstitution cp

        -- v is x applied to the context variables
        v <- case _A of
               Maybe Type
Nothing -> Sort -> Term
Sort (Sort -> Term) -> ([Arg Term] -> Sort) -> [Arg Term] -> 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) -> ([Arg Term] -> Elims) -> [Arg Term] -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> TCMT IO [Arg Term] -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m [Arg Term]
getMetaContextArgs MetaVariable
mv
               Just{}  -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Term) -> TCMT IO [Arg Term] -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaVariable -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m [Arg Term]
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 σ   = Int -> Substitution' Term
sub (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
_Θ)
            --    Γ <- Γ (r : GenTel) Δ <- Γ₀ (r : GenTel) <- Γ₀
            γ   = Impossible -> Int -> Substitution' Term
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' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' Term
δ Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1
            _Θγ = Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
γ Tele (Dom Type)
_Θ
            _Δσ = Substitution' (SubstArg (Tele (Dom Type)))
-> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Tele (Dom Type)))
σ Tele (Dom Type)
_Δ

        -- The substitution into the new context is simply lifting σ over Δ:
        --   Γ Θγ Δσ ⊢ lift i σ : Γ (r : GenTel) Δ
        let ρ  = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i Substitution' Term
σ
            -- We also need ρ⁻¹, which is a lot easier to construct.
            ρ' = Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
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' (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
_Θ) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ [QName]
genRecFields ] [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
1

        reportSDoc "tc.generalize.prune" 30 $ nest 2 $ vcat
          [ "Γ   =" <+> pretty _Γ
          , "Θ   =" <+> pretty _Θ
          , "Δ   =" <+> pretty _Δ
          , "σ   =" <+> pretty σ
          , "γ   =" <+> pretty γ
          , "δ   =" <+> pretty δ
          , "ρ   =" <+> pretty ρ
          , "ρ⁻¹ =" <+> pretty ρ'
          , "Θγ  =" <+> pretty _Θγ
          , "Δσ  =" <+> pretty _Δσ
          , "_A  =" <+> pretty _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 Θ.
        (newCxt, rΘ) <- do
          (rΔ, CxExtend _ rΓ) <- cxSplitAt i <$> getContext
          let setName dom :: Dom' Term (a, Type)
dom@(Dom' Term (a, Type) -> (a, Type)
forall t e. Dom' t e -> e
unDom -> (a
s,Type
ty)) = Name -> Dom Type -> ContextEntry
CtxVar (Name -> Dom Type -> ContextEntry)
-> f Name -> f (Dom Type -> ContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => a -> m Name
freshName_ a
s f (Dom Type -> ContextEntry) -> f (Dom Type) -> f ContextEntry
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Dom Type -> f (Dom Type)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dom Type -> f (Dom Type)) -> Dom Type -> f (Dom Type)
forall a b. (a -> b) -> a -> b
$ Dom' Term (a, Type)
dom Dom' Term (a, Type) -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
ty)
          rΘ <- mapM setName $ reverse $ telToList _Θγ
          let rΔσ = (Name -> Dom' Term ([Char], Type) -> ContextEntry)
-> [Name] -> [Dom' Term ([Char], Type)] -> [ContextEntry]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\ Name
name Dom' Term ([Char], Type)
dom -> Name -> Dom Type -> ContextEntry
CtxVar Name
name (([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term ([Char], Type)
dom))
                            ((ContextEntry -> Name) -> [ContextEntry] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' ContextEntry -> Name
ctxEntryName [ContextEntry]
rΔ)
                            ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. [a] -> [a]
reverse ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
_Δσ)
          return (cxPrepend rΔσ  $ cxPrepend rΘ rΓ, rΘ)

        -- Now we can enter the new context and create our meta variable.
        (y, u) <- updateContext ρ (const newCxt) $ localScope $ do

          -- First, we add the named variables to the scope, to allow
          -- them to be used in holes (#3341). These should go outside Δ (#3735).
          outsideLocalVars i $ addNamedVariablesToScope rΘ

          -- Now we can create the new meta
          newMetaFromOld mv ρ _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ρ' = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
ρ' Term
u
        reportSDoc "tc.generalize.prune" 80 $ vcat
          [ "solving"
          , nest 2 $ sep [ pretty v   <+> "=="
                         , pretty uρ' <+> ":"
                         , pretty _A ] ]
        noConstraints (doPrune x mv _A v uρ') `catchError` niceError x v

        reportSDoc "tc.generalize.prune" 80 $ vcat
          [ "solved"
          , nest 2 $ "v    =" <+> (pretty =<< instantiateFull v)
          , nest 2 $ "uρ⁻¹ =" <+> (pretty =<< instantiateFull uρ') ]

        setInteractionPoint x y

    findGenRec :: MetaVariable -> TCM (Maybe Int)
    findGenRec :: MetaVariable -> TCMT IO (Maybe Int)
findGenRec MetaVariable
mv = do
      cxt <- Context -> TCMT IO Context
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Context -> TCMT IO Context) -> TCMT IO Context -> TCMT IO Context
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      let n         = Context -> Int
forall a. Context' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
cxt
          notPruned = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
forall a b. (a -> b) -> a -> b
$
                      Permutation -> [Int] -> [Int]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP Int
n (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. Integral a => a -> [a]
downFrom Int
n
      case [ i
           | (i, CtxVar _ ((unDom -> (El _ (Def q _))))) <-
             cxWithIndex (,) cxt
           , q == genRecName
           , i `VarSet.member` notPruned
           ] of
        []    -> Maybe Int -> TCMT IO (Maybe Int)
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
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' Term -> Maybe Type -> TCM (MetaId, Term)
newMetaFromOld MetaVariable
mv Substitution' Term
ρ 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@(MetaS y _) <- TCM Sort
newSortMeta
          return (y, 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' Term
Substitution' (SubstArg Type)
ρ Type
_A
          RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> TCM (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck
                            (MetaInfo -> [Char]
miNameSuggestion (MetaInfo -> [Char]) -> MetaInfo -> [Char]
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 -> TCM ()
    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 -> [Arg Term] -> Term -> CompareAs -> TCMT IO ()
assign CompareDirection
DirEq MetaId
x (Term -> [Arg Term]
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 ()
equalSort (Term -> Sort
unwrapSort Term
v) (Term -> Sort
unwrapSort Term
u)
        Just Type
t     -> Type -> Term -> Term -> TCMT IO ()
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 -> [Arg Term]
getArgs = \case
            Sort (MetaS MetaId
_ Elims
es) -> Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
            MetaV MetaId
_ Elims
es        -> Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
            Term
_                 -> [Arg Term]
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 -> TCM a
    niceError :: forall a. MetaId -> Term -> TCErr -> TCM a
niceError MetaId
x Term
u TCErr
err = do
      u <- Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
u
      let 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 = cl{ clEnv = (clEnv cl) & eCall .~ Nothing }}
                   TCErr
_ -> TCErr
err
          telList = Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
genTel
          names   = (Dom' Term ([Char], Type) -> [Char])
-> [Dom' Term ([Char], Type)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char])
-> (Dom' Term ([Char], Type) -> ([Char], Type))
-> Dom' Term ([Char], Type)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom) [Dom' Term ([Char], Type)]
telList
          late    = (Dom' Term ([Char], Type) -> [Char])
-> [Dom' Term ([Char], Type)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map' (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char])
-> (Dom' Term ([Char], Type) -> ([Char], Type))
-> Dom' Term ([Char], Type)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term ([Char], Type)] -> [[Char]])
-> [Dom' Term ([Char], Type)] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Dom' Term ([Char], Type) -> Bool)
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Any -> Bool
getAny (Any -> Bool)
-> (Dom' Term ([Char], Type) -> Any)
-> Dom' Term ([Char], Type)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Any) -> Dom' Term ([Char], Type) -> Any
forall m.
Monoid m =>
(MetaId -> m) -> Dom' Term ([Char], Type) -> m
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 ([Char], Type)]
telList
          projs (Proj ProjOrigin
_ QName
q)
            | QName
q QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
genRecFields
            , Just [Char]
y <- QName -> Maybe [Char]
getGeneralizedFieldName QName
q
            = [Char] -> Set [Char]
forall a. a -> Set a
Set.singleton [Char]
y
          projs Elim' Term
_ = Set [Char]
forall a. Set a
Set.empty
          early = ((Term -> Set [Char]) -> Term -> Set [Char])
-> Term -> (Term -> Set [Char]) -> Set [Char]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Term -> Set [Char]) -> Term -> Set [Char]
forall m. Monoid m => (Term -> m) -> Term -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term
u \case
                  Var Int
_ Elims
es   -> (Elim' Term -> Set [Char]) -> Elims -> Set [Char]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set [Char]
projs Elims
es
                  Def QName
_ Elims
es   -> (Elim' Term -> Set [Char]) -> Elims -> Set [Char]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set [Char]
projs Elims
es
                  MetaV MetaId
_ Elims
es -> (Elim' Term -> Set [Char]) -> Elims -> Set [Char]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Elim' Term -> Set [Char]
projs Elims
es
                  Term
_          -> Set [Char]
forall a. Set a
Set.empty
          commas []       = [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
          commas [[Char]
x]      = [Char]
x
          commas [[Char]
x, [Char]
y]   = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
", and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
y
          commas ([Char]
x : [[Char]]
xs) = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [[Char]] -> [Char]
commas [[Char]]
xs
          cause = [Char]
"There were unsolved constraints that obscured the " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                  [Char]
"dependencies between the generalized variables."
          solution = [Char]
"The most reliable solution is to provide enough information to make the dependencies " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [Char]
"clear, but simply mentioning the variables in the right order should also work."
          order = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Dependency analysis suggested this (likely incorrect) order:",
                        Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([[Char]] -> [Char]
unwords [[Char]]
names) ]
          guess = [[Char]] -> [Char]
unwords
            [ [Char]
"After constraint solving it looks like", [[Char]] -> [Char]
commas [[Char]]
late
            , [Char]
"actually"
            , [[Char]]
-> ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
singPlural [[Char]]
late ([Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"s") [Char] -> [Char]
forall a. a -> a
id [Char]
"depend"  -- NB: this is a singular "s"
            , [Char]
"on", [[Char]] -> [Char]
commas ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ Set [Char] -> [[Char]]
forall a. Set a -> [a]
Set.toList Set [Char]
early
            ]
      typeError . GeneralizationFailed =<< vcat
        [ fwords $ "Variable generalization failed."
        , nest 2 $ sep ["- Probable cause", nest 4 $ fwords cause]
        , nest 2 $ sep ["- Suggestion", nest 4 $ fwords solution]
        , nest 2 $ sep $ ["- Further information"
                         , nest 2 $ "-" <+> order ] ++
                         [ nest 2 $ "-" <+> fwords guess | not (null late), not (null early) ] ++
                         [ nest 2 $ "-" <+> sep [ fwords "The dependency error is", prettyTCM err' ] ]
        ]

    addNamedVariablesToScope :: [ContextEntry] -> TCM ()
    addNamedVariablesToScope :: [ContextEntry] -> TCMT IO ()
addNamedVariablesToScope [ContextEntry]
cxt =
      [ContextEntry] -> (ContextEntry -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ContextEntry]
cxt ((ContextEntry -> TCMT IO ()) -> TCMT IO ())
-> (ContextEntry -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (CtxVar Name
x Dom Type
_) -> do
        -- Recognize named variables by lack of '.' (TODO: hacky!)
        [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.generalize.eta.scope" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Adding (or not) " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> Name
nameConcrete Name
x) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" to the scope"
        Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Char
'.' Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> Name
nameConcrete Name
x)) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.generalize.eta.scope" Int
40 [Char]
"  (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' Term
unpackSub ConHead
con [ArgInfo]
infos Int
i = Substitution' Term
recSub
  where
    ar :: Int
ar = [ArgInfo] -> Int
forall a. [a] -> 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' Term
recSub = Term
recVal Term -> Substitution' Term -> Substitution' Term
forall a. a -> Substitution' a -> Substitution' a
:# Int -> Substitution' Term -> Substitution' Term
forall a. Int -> Substitution' a -> Substitution' a
Wk Int
i Substitution' Term
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 MetaNameSuggestion, Type)] -> Telescope
buildGeneralizeTel :: ConHead -> [(Arg [Char], Type)] -> Tele (Dom Type)
buildGeneralizeTel ConHead
con [(Arg [Char], Type)]
xs = Int -> [(Arg [Char], Type)] -> Tele (Dom Type)
go Int
0 [(Arg [Char], Type)]
xs
  where
    infos :: [ArgInfo]
infos = ((Arg [Char], Type) -> ArgInfo)
-> [(Arg [Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg [Char] -> ArgInfo
forall e. Arg e -> ArgInfo
argInfo (Arg [Char] -> ArgInfo)
-> ((Arg [Char], Type) -> Arg [Char])
-> (Arg [Char], Type)
-> ArgInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg [Char], Type) -> Arg [Char]
forall a b. (a, b) -> a
fst) [(Arg [Char], Type)]
xs
    recSub :: Int -> Substitution' Term
recSub Int
i = ConHead -> [ArgInfo] -> Int -> Substitution' Term
unpackSub ConHead
con [ArgInfo]
infos Int
i
    go :: Int -> [(Arg [Char], Type)] -> Tele (Dom Type)
go Int
_ [] = Tele (Dom Type)
forall a. Tele a
EmptyTel
    go Int
i ((Arg [Char]
name, Type
ty) : [(Arg [Char], Type)]
xs) = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
dom Type
ty') (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs (Arg [Char] -> [Char]
forall e. Arg e -> e
unArg Arg [Char]
name) (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Int -> [(Arg [Char], Type)] -> Tele (Dom Type)
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Arg [Char], Type)]
xs
      where ty' :: Type
ty' = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' Term
recSub Int
i) Type
ty
            dom :: Type -> Dom Type
dom = ArgInfo -> [Char] -> Type -> Dom Type
forall a. ArgInfo -> [Char] -> a -> Dom a
defaultNamedArgDom (Arg [Char] -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg [Char]
name) (Arg [Char] -> [Char]
forall e. Arg e -> e
unArg Arg [Char]
name)

-- | Create metas for all used generalizable variables and their dependencies.
createGenValues ::
     Set QName
       -- ^ Possibly empty set of generalizable variables.
  -> TCM (Map MetaId QName, Map QName GeneralizedValue)
       -- ^ A bimap from generalizable variables to their metas.
createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues Set QName
s = do
  genvals <- Lens' TCEnv DoGeneralize
-> (DoGeneralize -> DoGeneralize)
-> TCMT IO [(QName, (MetaId, GeneralizedValue))]
-> TCMT IO [(QName, (MetaId, GeneralizedValue))]
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (DoGeneralize -> f DoGeneralize) -> TCEnv -> f TCEnv
Lens' TCEnv DoGeneralize
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]
-> (QName -> TCMT IO (QName, (MetaId, GeneralizedValue)))
-> TCMT IO [(QName, (MetaId, GeneralizedValue))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((QName -> QName -> Ordering) -> [QName] -> [QName]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Range' SrcFile -> Range' SrcFile -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range' SrcFile -> Range' SrcFile -> Ordering)
-> (QName -> Range' SrcFile) -> QName -> QName -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` QName -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
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) \ QName
x -> do
      (QName
x,) ((MetaId, GeneralizedValue) -> (QName, (MetaId, GeneralizedValue)))
-> TCMT IO (MetaId, GeneralizedValue)
-> TCMT IO (QName, (MetaId, GeneralizedValue))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (MetaId, GeneralizedValue)
createGenValue QName
x
  let 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 = (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 ]
  return (metaMap, nameMap)

-- | Create a generalizable meta for a generalizable variable.
createGenValue ::
     QName
       -- ^ Name of a generalizable variable.
  -> TCM (MetaId, GeneralizedValue)
       -- ^ Generated metavariable and its representation as typed term.
createGenValue :: QName -> TCMT IO (MetaId, GeneralizedValue)
createGenValue QName
x = QName
-> TCMT IO (MetaId, GeneralizedValue)
-> TCMT IO (MetaId, GeneralizedValue)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (TCMT IO (MetaId, GeneralizedValue)
 -> TCMT IO (MetaId, GeneralizedValue))
-> TCMT IO (MetaId, GeneralizedValue)
-> TCMT IO (MetaId, GeneralizedValue)
forall a b. (a -> b) -> a -> b
$ do
  cp  <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint

  def <- instantiateDef =<< getConstInfo x
  let
    nGen = case Definition -> Defn
theDef Definition
def of
      GeneralizableVar NumGeneralizableArgs
NoGeneralizableArgs       -> Int
0
      GeneralizableVar (SomeGeneralizableArgs Int
n) -> Int
n
      Defn
_ -> Int
forall a. HasCallStack => a
__IMPOSSIBLE__

    ty         = Definition -> Type
defType Definition
def
    TelV tel _ = telView' ty
    -- Generalizable variables are never explicit, so if they're given as
    -- explicit we default to hidden.
    argTel     = [Dom' Term ([Char], Type)] -> Tele (Dom Type)
telFromList ([Dom' Term ([Char], Type)] -> Tele (Dom Type))
-> [Dom' Term ([Char], Type)] -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ (Dom' Term ([Char], Type) -> Dom' Term ([Char], Type))
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term ([Char], Type) -> Dom' Term ([Char], Type)
forall a. LensHiding a => a -> a
hideExplicit ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. Int -> [a] -> [a]
take' Int
nGen ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel

  args <- newTelMeta argTel
  metaType <- piApplyM ty args

  let name = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
  (m, term) <- newNamedValueMeta DontRunMetaOccursCheck name CmpLeq 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.
  updateMetaVar m $ \ MetaVariable
mv ->
    Modality -> MetaVariable -> MetaVariable
forall a. LensModality a => Modality -> a -> a
setModality (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality (Definition -> ArgInfo
defArgInfo Definition
def)) (MetaVariable -> MetaVariable) -> MetaVariable -> MetaVariable
forall a b. (a -> b) -> a -> b
$
    MetaVariable
mv { mvFrozen = Frozen }

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

  reportSDoc "tc.generalize" 50 $ vcat
    [ "created metas for generalized variable" <+> prettyTCM x
    , nest 2 $ "top  =" <+> prettyTCM term
    , nest 2 $ "args =" <+> prettyTCM args ]

  case term of
    MetaV{} -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Term
_       -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TypeError
CannotGeneralizeEtaExpandable QName
x Type
metaType

  return . (m,) $ GeneralizedValue
    { genvalCheckpoint = cp
    , genvalTerm       = term
    , genvalType       = metaType
    }

  where
    hideExplicit :: LensHiding a => a -> a
    hideExplicit :: forall a. LensHiding a => a -> a
hideExplicit = (a -> Bool) -> (a -> a) -> a -> a
forall b a. IsBool b => (a -> b) -> (a -> a) -> a -> a
applyWhenIts a -> Bool
forall a. LensHiding a => a -> Bool
visible a -> a
forall a. LensHiding a => a -> a
hide


-- | 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 = TCMT IO (QName, ConHead, [QName])
-> TCMT IO (QName, ConHead, [QName])
forall a. TCM a -> TCM a
noMutualBlock (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
$ do
  current <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  let freshQName [Char]
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
<$> [Char] -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => [Char] -> m Name
freshName_ ([Char]
s :: String)
      mkFieldName  = [Char] -> TCMT IO QName
freshQName ([Char] -> TCMT IO QName)
-> ([Char] -> [Char]) -> [Char] -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
generalizedFieldName [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> TCMT IO QName)
-> (MetaId -> TCMT IO [Char]) -> MetaId -> TCMT IO QName
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< MetaId -> TCMT IO [Char]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion
  genRecFields <- mapM (defaultDom <.> mkFieldName) sortedMetas
  genRecName   <- freshQName generalizeRecordName
  genRecCon    <- freshQName generalizeConstructorName <&> \ QName
con -> ConHead
                  { conName :: QName
conName      = QName
con
                  , conDataRecord :: DataOrRecord
conDataRecord= PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
CopatternMatching
                  , conInductive :: Induction
conInductive = Induction
Inductive
                  , conFields :: [Arg QName]
conFields    = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
genRecFields
                  }
  projIx <- succ . size <$> getContext
  erasure <- optErasure <$> pragmaOptions
  inTopContext $ forM_ (zip' sortedMetas genRecFields) $ \ (MetaId
meta, Dom' Term QName
fld) -> do
    fieldTy <- MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
meta
    let field = Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom Dom' Term QName
fld
    addConstant' field (getArgInfo fld) fieldTy $ FunctionDefn $
      (emptyFunctionData_ erasure)
        { _funMutual     = Just []
        , _funTerminates = Just True
        , _funProjection = Right Projection
          { projProper   = Just genRecName
          , projOrig     = field
          , projFromType = defaultArg genRecName
          , projIndex    = projIx
          , projLams     = ProjLams [defaultArg "gtel"]
          }
        }
  addConstant' (conName genRecCon) defaultArgInfo __DUMMY_TYPE__ $ -- Filled in later
    Constructor { conPars   = 0
                , conArity  = length genRecFields
                , conSrcCon = genRecCon
                , conData   = genRecName
                , conAbstr  = ConcreteDef
                , conComp   = emptyCompKit
                , conProj   = Nothing
                , conForced = []
                , conErased = Nothing
                , conErasure = erasure
                , conInline  = False
                }
  let dummyTel a
0 = Tele (Dom Type)
forall a. Tele a
EmptyTel
      dummyTel a
n = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
HasCallStack => Type
__DUMMY_TYPE__) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ [Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. [Char] -> a -> Abs a
Abs [Char]
"_" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ a -> Tele (Dom Type)
dummyTel (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
  addConstant' genRecName defaultArgInfo (sort genRecSort) $
    Record { recPars         = 0
           , recClause       = Nothing
           , recConHead      = genRecCon
           , recNamedCon     = False
           , recFields       = genRecFields
           , recTel          = dummyTel (length genRecFields) -- Filled in later
           , recMutual       = Just []
           , recPositivityCheck = NoPositivityCheck
           , recEtaEquality' = EtaEquality YesEta EtaFromPragma
           , recPatternMatching = CopatternMatching
           , recInduction    = Nothing
           , recTerminates   = Just True    -- not recursive
           , recAbstr        = ConcreteDef
           , recComp         = emptyCompKit
           }
  reportSDoc "tc.generalize" 20 $ vcat
    [ text "created genRec" <+> prettyList_ (map' (text . prettyShow . unDom) genRecFields) ]
  reportSDoc "tc.generalize" 80 $ vcat
    [ text "created genRec" <+> text (prettyShow genRecFields) ]
  -- Solve the genRecMeta
  args <- getContextArgs
  let 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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args
  noConstraints $ equalType genRecTy genRecMeta
  return (genRecName, genRecCon, map' unDom 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 -> Tele (Dom Type) -> TCMT IO ()
fillInGenRecordDetails QName
name ConHead
con [QName]
fields Type
recTy Tele (Dom Type)
fieldTel = do
  cxtTel <- (Dom Type -> Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall a b. (a -> b) -> Tele a -> Tele b
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 (Tele (Dom Type) -> Tele (Dom Type))
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope
  let fullTel = Tele (Dom Type)
cxtTel Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Tele (Dom Type)
fieldTel
  -- Field types
  let mkFieldTypes [] Tele (Dom Type)
EmptyTel = []
      mkFieldTypes (QName
fld : [QName]
flds) (ExtendTel Dom Type
ty Abs (Tele (Dom Type))
ftel) =
          Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
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) ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
Abs [Char]
"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] -> Tele (Dom Type) -> [Type]
mkFieldTypes [QName]
flds (Abs (Tele (Dom Type))
-> SubstArg (Tele (Dom Type)) -> Tele (Dom Type)
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs (Tele (Dom Type))
ftel Term
SubstArg (Tele (Dom Type))
proj)
        where
          s :: Sort
s = Dom Type -> Abs Type -> Sort
mkPiSort (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
recTy) ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
Abs [Char]
"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]
_ Tele (Dom Type)
_ = [Type]
forall a. HasCallStack => a
__IMPOSSIBLE__
  let fieldTypes = [QName] -> Tele (Dom Type) -> [Type]
mkFieldTypes [QName]
fields (Int -> Tele (Dom Type) -> Tele (Dom Type)
forall a. Subst a => Int -> a -> a
raise Int
1 Tele (Dom Type)
fieldTel)
  reportSDoc "tc.generalize" 40 $ text "Field types:" <+> inTopContext (nest 2 $ vcat $ map' prettyTCM fieldTypes)
  zipWithM_ setType fields fieldTypes
  -- Constructor type
  let conType = Tele (Dom Type)
fullTel Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
`abstract` Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
fieldTel) Type
recTy
  reportSDoc "tc.generalize" 40 $ text "Final genRecCon type:" <+> inTopContext (prettyTCM conType)
  setType (conName con) conType
  -- Record telescope: Includes both parameters and fields.
  modifyGlobalDefinition name $ set (lensTheDef . lensRecord . lensRecTel) fullTel
  -- #7380: Also add clauses to the field definitions
  let n      = [QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
fields
      cpi    = ConPatternInfo
noConPatternInfo
      fldTys = (Dom' Term ([Char], Type) -> Arg Type)
-> [Dom' Term ([Char], Type)] -> [Arg Type]
forall a b. (a -> b) -> [a] -> [b]
map' ((([Char], Type) -> Type) -> Arg ([Char], Type) -> Arg Type
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> Type
forall a b. (a, b) -> b
snd (Arg ([Char], Type) -> Arg Type)
-> (Dom' Term ([Char], Type) -> Arg ([Char], Type))
-> Dom' Term ([Char], Type)
-> Arg Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term ([Char], Type) -> Arg ([Char], Type)
forall t a. Dom' t a -> Arg a
argFromDom) ([Dom' Term ([Char], Type)] -> [Arg Type])
-> [Dom' Term ([Char], Type)] -> [Arg Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
fieldTel
      conPat = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
-> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$! ((Int, Arg Type) -> NamedArg (Pattern' DBPatVar))
-> [(Int, Arg Type)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> [a] -> [b]
map' (\(Int
i, Arg Type
arg) -> (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a name. a -> Named name a
unnamed (Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar))
-> Arg (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Pattern' DBPatVar
forall a. a -> Pattern' a
varP ([Char] -> Int -> DBPatVar
DBPatVar [Char]
"x" Int
i) Pattern' DBPatVar -> Arg Type -> Arg (Pattern' DBPatVar)
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Type
arg) ([Int] -> [Arg Type] -> [(Int, Arg Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip' (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) [Arg Type]
fldTys)
  forM_ (zip3 (downFrom n) fields fldTys) \ (Int
i, QName
fld, Arg Type
fldTy) -> do
    QName -> ([Clause] -> [Clause]) -> TCMT IO ()
modifyFunClauses QName
fld \ [Clause]
_ ->
      [Clause
        { clauseLHSRange :: Range' SrcFile
clauseLHSRange    = Range' SrcFile
forall a. Range' a
noRange
        , clauseFullRange :: Range' SrcFile
clauseFullRange   = Range' SrcFile
forall a. Range' a
noRange
        , clauseTel :: Tele (Dom Type)
clauseTel         = Tele (Dom Type)
fieldTel
        , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats   = [Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a. a -> NamedArg a
defaultNamedArg Pattern' DBPatVar
conPat]
        , clauseBody :: Maybe Term
clauseBody        = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
        , clauseType :: Maybe (Arg Type)
clauseType        = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Int -> Arg Type -> Arg Type
forall a. Subst a => Int -> a -> a
raise (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Arg Type
fldTy
        , clauseCatchall :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
        , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive
        , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
        , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
        }]
  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 = ty }