Agda-2.8.0: src/full/Agda/TypeChecking/InstanceArguments.hs
{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.InstanceArguments
( findInstance
, isInstanceConstraint
, solveAwakeInstanceConstraints
, shouldPostponeInstanceSearch
, postponeInstanceConstraints
, flushInstanceConstraints
, getInstanceCandidates
, getInstanceDefs
, OutputTypeName(..)
, getOutputTypeName
, addTypedInstance
, readdTypedInstance
, addTypedInstance'
, pruneTemporaryInstances
, resolveInstanceHead
) where
import Control.Monad.Except (ExceptT(..), runExceptT, MonadError(..))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Function (on)
import Data.Monoid hiding ((<>))
import Data.Foldable (toList, foldrM)
import Agda.Interaction.Options (optQualifiedInstances, lensOptExperimentalLazyInstances)
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (isQualified)
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName', AllowAmbiguousNames(..))
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion.Pure (pureEqualTermB)
import Agda.TypeChecking.Errors () --instance only
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Datatypes
import {-# SOURCE #-} Agda.TypeChecking.Constraints
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import qualified Agda.Benchmarking as Benchmark
import Agda.TypeChecking.Monad.Benchmark (billTo)
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Syntax.Common.Pretty (prettyShow)
import qualified Agda.Utils.ProfileOptions as Profile
-- import qualified Agda.Utils.HashTable as HashTable
import Agda.Utils.WithDefault (lensCollapseDefault)
import Agda.Utils.Impossible
-- import Agda.Utils.HashTable (HashTable)
import Agda.TypeChecking.DiscrimTree
-- import GHC.IO (unsafePerformIO)
-- | Compute a list of instance candidates.
-- 'Nothing' if target type or any context type is a meta, error if
-- type is not eligible for instance search.
initialInstanceCandidates :: Bool -> Type -> TCM (Either Blocker [Candidate])
initialInstanceCandidates blockOverlap instTy = do
(_, _, otn) <- getOutputTypeName instTy
case otn of
NoOutputTypeName -> typeError $ InvalidInstanceHeadType instTy ImproperInstHead
OutputTypeVisiblePi -> typeError $ InvalidInstanceHeadType instTy ImproperInstTele
OutputTypeNameNotYetKnown b -> do
reportSDoc "tc.instance.cands" 30 $ "Instance type is not yet known. "
return (Left b)
OutputTypeVar -> do
reportSDoc "tc.instance.cands" 30 $ "Instance type is a variable. "
runBlocked (getContextCands Nothing)
OutputTypeName n -> Bench.billTo [Bench.Typing, Bench.InstanceSearch, Bench.InitialCandidates] do
reportSDoc "tc.instance.cands" 30 $ "Found instance type head: " <+> prettyTCM n
runBlocked do
local <- getContextCands (Just n)
global <- getScopeDefs n
lift $ tickCandidates n $ length local + length global
pure $ local <> global
where
-- Ticky profiling for statistics about a class.
tickCandidates n size = whenProfile Profile.Instances do
n <- prettyTCM n
let pref = "class " <> show n
-- Number of instance constraints of this class that have gotten a
-- set of candidates
tick $ pref <> ": attempts"
-- Per-class info: number of constraints where there was only one
-- candidate (awesome) + the total number of candidates we've gone
-- through.
when (size == 1) $ tick $ pref <> ": only one candidate"
when (size >= 1) $ tickN
(pref <> ": total candidates visited")
(fromIntegral size)
-- get a list of variables with their type, relative to current context
getContextCands :: Maybe QName -> BlockT TCM [Candidate]
getContextCands cls = do
ctx <- getContext
reportSDoc "tc.instance.cands" 40 $ hang "Getting candidates from context" 2 (inTopContext $ prettyTCM $ PrettyContext ctx)
-- Context variables with their types lifted to live in the full context
let varsAndRaisedTypes = reverse $ zip (contextTerms ctx) (flattenTel $ contextToTel ctx)
vars = [ Candidate LocalCandidate x t (infoOverlapMode info)
| (x, Dom{domInfo = info, unDom = t}) <- varsAndRaisedTypes
, isInstance info
]
-- {{}}-fields of variables are also candidates
let cxtAndTypes = [ (LocalCandidate, x, t) | (x, Dom{unDom = t}) <- varsAndRaisedTypes ]
fields <- concat <$> mapM instanceFields (reverse cxtAndTypes)
reportSDoc "tc.instance.fields" 30 $
if null fields then "no instance field candidates" else
"instance field candidates" $$ do
nest 2 $ vcat (map debugCandidate fields)
-- get let bindings
env <- asksTC envLetBindings
env <- mapM (traverse getOpen) $ Map.toList env
let lets = [ Candidate LocalCandidate v t DefaultOverlap
| (_, LetBinding _ v Dom{domInfo = info, unDom = t}) <- env
, isInstance info
, usableModality info
]
filterM (sameHead cls . candidateType) $ vars ++ fields ++ lets
sameHead :: Maybe QName -> Type -> BlockT TCM Bool
sameHead Nothing _ = pure True
sameHead (Just cls) t = lift (thd3 <$> getOutputTypeName t) >>= \case
OutputTypeName inst -> pure (inst == cls)
OutputTypeNameNotYetKnown b -> patternViolation b
_ -> pure False
infoOverlapMode :: LensArgInfo a => a -> OverlapMode
infoOverlapMode info = if isYesOverlap (getArgInfo info) then FieldOverlap else DefaultOverlap
etaExpand :: (MonadTCM m, PureTCM m)
=> Bool -> Type -> m (Maybe (QName, Args))
etaExpand etaOnce t =
isEtaRecordType t >>= \case
Nothing | etaOnce -> do
isRecordType t >>= \case
Nothing -> return Nothing
Just (r, vs, _) -> do
m <- currentModule
-- Are we inside the record module? If so it's safe and desirable
-- to eta-expand once (issue #2320).
if qnameToList0 r `List.isPrefixOf` mnameToList m
then return (Just (r, vs))
else return Nothing
r -> return r
instanceFields :: (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
instanceFields = instanceFields' True
instanceFields' :: Bool -> (CandidateKind,Term,Type) -> BlockT TCM [Candidate]
instanceFields' etaOnce (q, v, t) =
ifBlocked t (\ m _ -> patternViolation m) $ \ _ t -> do
caseMaybeM (etaExpand etaOnce t) (return []) $ \ (r, pars) -> do
(tel, args) <- lift $ forceEtaExpandRecord r pars v
let types = map unDom $ applySubst (parallelS $ reverse $ map unArg args) (flattenTel tel)
fmap concat $ forM (zip args types) $ \ (arg, t) ->
([ Candidate LocalCandidate (unArg arg) t (infoOverlapMode arg)
| isInstance arg
] ++) <$>
instanceFields' False (LocalCandidate, unArg arg, t)
-- Compute whether we should block this instance constraint at the
-- discrimination tree stage.
shouldBlockOverlap :: Blocker -> Set.Set QName -> TCM Bool
shouldBlockOverlap bs cands = do
let
recursive = useTC stConsideringInstance
hack = useTC stInstanceHack
enabled = useTC (stPragmaOptions . lensOptExperimentalLazyInstances . lensCollapseDefault)
mutual = caseMaybeM (asksTC envMutualBlock) (pure mempty) \ mb ->
mutualNames <$> lookupMutualBlock mb
andM
[ pure blockOverlap
-- For the getInstances reflection primitive, we don't want
-- to block on overlap, so that the user can do their thing.
, enabled
-- Also disable it depending on the pragma option.
, pure $ not $ Set.null $ allBlockingMetas bs
-- Don't block if there's no metas to block on
, pure $ natSize cands > 1
-- It's possible that the discrimination tree forced a
-- metavariable even if there's exactly one candidate. In this
-- case, we should not block, because this instance constraint
-- might be the only thing that can solve the blocking metas.
, not <$> hack
-- To support 'inert improvement' (see ImproveInertRHS), we
-- try all the candidates even if the discrimination tree
-- thinks that there will be overlap. This is because it's
-- possible we have e.g.
--
-- instance ?1 : Foo ?0, candidates {Foo T, Foo S}
-- blocker ?0
-- ?0 X = T X (blocked on ?0)
--
-- If we block ?1 on ?0 again (as we would've done during the
-- body), then both of these go unsolved. But if we try all
-- the candidates, we'll see that 'Foo T' is the only possible
-- candidate, thus solving both constraints.
, mutual <&> (`Set.disjoint` cands)
-- Work around for #7186: the result of termination checking
-- depends on whether we solve instance metas eagerly or late.
-- Consider
--
-- instance Show-List = record { show = go }
-- go (x ∷ xs) = show x <> show ⦃ ?0 ⦄ xs
--
-- If we solve ?0 eagerly, the term we use is the literal
-- record constructor. The 'show' projection unfolds in 'go'
-- and the termination check is happy.
--
-- If we solve it late, we run the risk of the clause
-- compiler applying copattern translation to Show-List. The
-- 'show' projection does not eagerly unfold, and the
-- termination check explodes.
, not <$> recursive
-- Blocking instance selection *on a meta* while considering
-- an instance causes the recursive instance constraint to
-- get repeatedly woken up. Not good for performance.
]
getScopeDefs :: QName -> BlockT TCM [Candidate]
getScopeDefs n = do
rel <- viewTC eRelevance
InstanceTable tree counts <- lift getInstanceDefs
QueryResult qs blocker <- lift $ lookupDT (unEl instTy) tree
reportSDoc "tc.instance.candidates.search" 20 $ vcat
[ "instance candidates from signature for goal:"
, nest 2 (prettyTCM =<< instantiateFull instTy)
, nest 2 (prettyTCM qs)
, "length:" <+> prettyTCM (length qs)
, "blocker:"
, nest 2 (prettyTCM blocker)
]
cands <- catMaybes <$> mapM (lift . candidate rel) (toList qs)
should <- lift (shouldBlockOverlap blocker qs)
when (length cands > 1 && should) do
reportSDoc "tc.instance.defer" 20 $ vcat
[ "Postponing because of discrimination tree overlap."
]
patternViolation blocker
-- Some more class-specific profiling.
lift $ whenProfile Profile.Instances case Map.lookup n counts of
Just tot -> do
n <- prettyTCM n
-- Record the overall total number of candidates that were
-- skipped by lookup in the discrimination tree, and record
-- this per-class, as well.
let diff = fromIntegral (tot - length cands)
tickN "instances discarded early" diff
tickN ("class " <> show n <> ": discarded early") diff
Nothing -> pure ()
pure cands
candidate :: Relevance -> QName -> TCM (Maybe Candidate)
candidate rel q = ifNotM (isNameInScope q <$> getScope) (return Nothing) $ do
-- Jesper, 2020-03-16: When using --no-qualified-instances,
-- filter out instances that are only in scope under a qualified
-- name.
filterQualified $ do
-- Andreas, 2012-07-07:
-- we try to get the info for q
-- while opening a module, q may be in scope but not in the signature
-- in this case, we just ignore q (issue 674)
flip catchError handle $ do
def <- getConstInfo q
if not (getRelevance def `moreRelevant` rel) then return Nothing else do
-- Andreas, 2017-01-14: instantiateDef is a bit of an overkill
-- if we anyway get the freeVarsToApply
-- WAS: t <- defType <$> instantiateDef def
args <- freeVarsToApply q
let
t = defType def `piApply` args
rel = getRelevance $ defArgInfo def
v = case theDef def of
-- drop parameters if it's a projection function...
Function{ funProjection = Right p } -> projDropParsApply p ProjSystem rel args
-- Andreas, 2014-08-19: constructors cannot be declared as
-- instances (at least as of now).
-- I do not understand why the Constructor case is not impossible.
-- Ulf, 2014-08-20: constructors are always instances.
Constructor{ conSrcCon = c } -> Con c ConOSystem []
_ -> Def q $ map Apply args
mode = case defInstance def of
Just i -> instanceOverlap i
Nothing -> DefaultOverlap
-- Amy, 2025-04-10: it's possible that an instance in the
-- discrimination tree has a type which, in the current
-- context, has visible quantifiers (e.g. because we're
-- outside the parametrised module it was defined in).
--
-- Discard them early so that they don't count towards
-- potentially blocking on "overlap".
TelV tele _ <- telView t
return do
guard (all (not . visible) tele)
Just $ Candidate (GlobalCandidate q) v t mode
where
-- unbound constant throws an internal error
handle (TypeError _ _ (Closure {clValue = InternalError _})) = return Nothing
handle err = throwError err
filterQualified :: TCM (Maybe Candidate) -> TCM (Maybe Candidate)
filterQualified m = ifM (optQualifiedInstances <$> pragmaOptions) m $ do
qc <- inverseScopeLookupName' AmbiguousAnything q <$> getScope
let isQual = maybe True isQualified $ listToMaybe qc
reportSDoc "tc.instance.qualified" 30 $
if isQual then
"dropping qualified instance" <+> prettyTCM q
else
"keeping instance" <+> prettyTCM q <+>
"since it is in scope as" <+> prettyTCM qc
if isQual then return Nothing else m
-- | @findInstance m (v,a)s@ tries to instantiate on of the types @a@s
-- of the candidate terms @v@s to the type @t@ of the metavariable @m@.
-- If successful, meta @m@ is solved with the instantiation of @v@.
-- If unsuccessful, the constraint is regenerated, with possibly reduced
-- candidate set.
-- The list of candidates is equal to @Nothing@ when the type of the meta
-- wasn't known when the constraint was generated. In that case, try to find
-- its type again.
findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
findInstance m Nothing = do
r <- getMetaRange m
ifM canDropRecursiveInstance (addConstraint neverUnblock (FindInstance r m Nothing)) $ do
-- Getting initial candidates can fail, in which case we should postpone (#7286)
catchConstraint (FindInstance r m Nothing) $ do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupLocalMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 20 $ "The type of the FindInstance constraint isn't known, trying to find it again."
t <- instantiate =<< getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInstance 1: t: " ++ prettyShow t
-- Issue #2577: If the target is a function type the arguments are
-- potential candidates, so we add them to the context to make
-- initialInstanceCandidates pick them up.
TelV tel t <- telViewUpTo' (-1) notVisible t
cands <- addContext tel $ initialInstanceCandidates True t
case cands of
Left unblock -> do
reportSLn "tc.instance" 20 "Can't figure out target of instance goal. Postponing constraint."
addConstraint unblock $ FindInstance r m Nothing
Right cs -> findInstance m (Just cs)
findInstance m (Just cands) = do -- Note: if no blocking meta variable this will not unblock until the end of the mutual block
r <- getMetaRange m
whenJustM (findInstance' m cands) $ (\ (cands, b) -> addConstraint b $ FindInstance r m $ Just cands)
-- | Entry point for `tcGetInstances` primitive
getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
getInstanceCandidates m = wrapper where
wrapper = do
mv <- lookupLocalMeta m
setCurrentRange mv $ do
t <- instantiate =<< getMetaTypeInContext m
TelV tel t' <- telViewUpTo' (-1) notVisible t
addContext tel $ runExceptT (worker t')
insertCandidate :: Candidate -> [Candidate] -> TCM [Candidate]
insertCandidate x [] = pure [x]
insertCandidate x (y:xs) = doesCandidateSpecialise x y >>= \case
True -> pure (x:y:xs)
False -> (y:) <$> insertCandidate x xs
worker :: Type -> ExceptT Blocker TCM [Candidate]
worker t' = do
cands <- ExceptT (initialInstanceCandidates False t')
cands <- lift (checkCandidates m t' cands) <&> \case
Nothing -> cands
Just (_, cands) -> fst <$> cands
cands <- Bench.billTo [Bench.Typing, Bench.InstanceSearch, Bench.OrderCandidates] $
lift (foldrM insertCandidate [] cands)
reportSDoc "tc.instance.sort" 20 $ nest 2 $
"sorted candidates" $$ vcat (map debugCandidate cands)
pure cands
-- | @'doesCandidateSpecialise' c1 c2@ checks whether the instance
-- candidate @c1@ /specialises/ the instance candidate @c2@, i.e.,
-- whether the type of @c2@ is a substitution instance of @c1@'s type.
--
-- Only the final return type of the instances is considered: the
-- presence of unsolvable instance arguments in the types of @c1@ or
-- @c2@ does not affect the results of 'doesCandidateSpecialise'.
doesCandidateSpecialise :: Candidate -> Candidate -> TCM Bool
doesCandidateSpecialise c1@Candidate{candidateType = t1} c2@Candidate{candidateType = t2} = do
whenProfile Profile.Instances $ tick "doesCandidateSpecialise"
-- We compare
-- c1 : ∀ {Γ} → T
-- against
-- c2 : ∀ {Δ} → S
-- by moving to the context Γ ⊢, so that any variables in T's type are
-- "rigid", but *instantiating* S[?/Δ], so its variables are
-- "flexible"; then calling the conversion checker.
let
handle e = do
reportSDoc "tc.instance.sort" 30 $ nest 2 "=> NOT specialisation"
reportSDoc "tc.instance.sort" 40 $ prettyTCM e
pure False
wrap = flip catchError handle
-- Turn failures into returning false
. localTCState
-- Discard any changes to the TC state (metas from
-- instantiating t2, recursive instance constraints, etc)
. locallyTCState stPostponeInstanceSearch (const True)
-- Don't spend any time looking for instances in the contexts
. nowConsideringInstance
-- Don't execute tactics either
TelV tel t1 <- telView t1
addContext tel $ wrap $ do
-- Amy, 2025-02-28: Have to raise the type of the other candidate to
-- live in t1's context!
(args, t2) <- implicitArgs (-1) (\h -> notVisible h) (raise (length tel) t2)
reportSDoc "tc.instance.sort" 30 $ "Does" <+> prettyTCM (raise (length tel) c1) <+> "specialise" <+> (prettyTCM (raise (length tel) c2) <> "?")
reportSDoc "tc.instance.sort" 60 $ vcat
[ "Comparing candidate"
, nest 2 (prettyTCM c1 <+> colon <+> prettyTCM t1)
, "vs"
, nest 2 (prettyTCM c2 <+> colon <+> prettyTCM t2)
]
leqType t2 t1
reportSDoc "tc.instance.sort" 30 $ nest 2 "=> IS specialisation"
pure True
-- | Checks whether an instance overlaps another. This involves a strict
-- specificity check (the new instance should be more specific than the
-- old instance but not vice-versa) and the consideration of whether
-- these instances are overlappable/overlapping at all.
--
-- Fails early if the new candidate is not overlapping and the old
-- candidate is not overlappable.
doesCandidateOverlap :: Candidate -> Candidate -> TCM Bool
doesCandidateOverlap new old = if isOverlapping new || isOverlappable old
then andM [ doesCandidateSpecialise new old
, fmap not (doesCandidateSpecialise old new) ]
else pure False
-- | Result says whether we need to add constraint, and if so, the set of
-- remaining candidates and an eventual blocking metavariable.
findInstance' :: MetaId -> [Candidate] -> TCM (Maybe ([Candidate], Blocker))
findInstance' m cands = do
let
frozen = do
reportSLn "tc.instance.defer" 20 "Refusing to solve frozen instance meta."
whenProfile Profile.Instances $ tick "findInstance: frozen"
return (Just (cands, neverUnblock))
recursive = do
recur <- useTC stConsideringInstance
reportSLn "tc.instance.defer" 20
if recur
then "Postponing recursive instance search."
else "Postponing possibly recursive instance search."
whenProfile Profile.Instances $ tick "findInstance: recursive"
return $ Just (cands, neverUnblock)
ifM (isFrozen m) frozen do
ifM shouldPostponeInstanceSearch recursive do
billTo [Benchmark.Typing, Benchmark.InstanceSearch] do
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupLocalMeta m
setCurrentRange mv $ do
reportSLn "tc.instance" 15 $
"findInstance 2: constraint: " ++ prettyShow m ++ "; candidates left: " ++ show (length cands)
reportSDoc "tc.instance" 60 $ nest 2 $ vcat $ map debugCandidate cands
reportSDoc "tc.instance" 70 $ "raw" $$ do
nest 2 $ vcat $ map debugCandidateRaw cands
t <- getMetaTypeInContext m
reportSLn "tc.instance" 70 $ "findInstance 2: t: " ++ prettyShow t
insidePi t $ \ t -> do
reportSDoc "tc.instance" 15 $ "findInstance 3: t =" <+> prettyTCM t
reportSLn "tc.instance" 70 $ "findInstance 3: t: " ++ prettyShow t
mcands <-
-- Temporarily remove other instance constraints to avoid
-- redundant solution attempts
holdConstraints (const isInstanceProblemConstraint) $
checkCandidates m t cands
debugConstraints
case mcands of
Just ([(_, err)], []) -> do
reportSDoc "tc.instance" 15 $
"findInstance 5: the only viable candidate failed..."
throwError err
Just (errs, []) -> do
if null errs then reportSDoc "tc.instance" 15 $ "findInstance 5: no viable candidate found..."
else reportSDoc "tc.instance" 15 $ "findInstance 5: all viable candidates failed..."
-- #3676: Sort the candidates based on the size of the range for the errors and
-- set the range of the full error to the range of the most precise candidate
-- error.
let sortedErrs = List.sortBy (compare `on` precision) errs
where precision (_, err) = maybe infinity iLength $ rangeToInterval $ getRange err
infinity = 1000000000
setCurrentRange (take 1 $ map snd sortedErrs) $
typeError $ InstanceNoCandidate t [ (candidateTerm c, err) | (c, err) <- sortedErrs ]
Just (errs, [(c@(Candidate q term t' _), v)]) -> do
reportSDoc "tc.instance" 15 $ vcat
[ "instance search: attempting"
, nest 2 $ prettyTCM m <+> ":=" <+> prettyTCM v
]
reportSDoc "tc.instance" 70 $ nest 2 $
"candidate v = " <+> pretty v
ctxElims <- map Apply <$> getContextArgs
equalTerm t (MetaV m ctxElims) v
reportSDoc "tc.instance" 15 $ vcat
[ "findInstance 5: solved by instance search using the only candidate"
, nest 2 $ prettyTCM c <+> "=" <+> prettyTCM term
, "of type " <+> prettyTCM t'
, "for type" <+> prettyTCM t
]
-- If we actually solved the constraints we should wake up any held
-- instance constraints, to make sure we don't forget about them.
wakeupInstanceConstraints
return Nothing -- We’re done
_ -> do
let cs = maybe cands (map fst . snd) mcands -- keep the current candidates if Nothing
reportSDoc "tc.instance" 15 $
text ("findInstance 5: refined candidates: ") <+>
prettyTCM (List.map candidateTerm cs)
whenProfile Profile.Instances $ tick "findInstance: multiple candidates"
return (Just (cs, neverUnblock))
insidePi :: Type -> (Type -> TCM a) -> TCM a
insidePi t ret = reduce (unEl t) >>= \case
Pi a b -> addContext (absName b, a) $ insidePi (absBody b) ret
Def{} -> ret t
Var{} -> ret t
Sort{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s
-- | Apply the computation to every argument in turn by resetting the state every
-- time. Return the list of the arguments giving the result True.
--
-- If the resulting list contains exactly one element, then the state is the
-- same as the one obtained after running the corresponding computation. In
-- all the other cases, the state is reset.
--
-- Also returns the candidates that pass type checking but fails constraints,
-- so that the error messages can be reported if there are no successful
-- candidates.
filterResettingState
:: MetaId
-> [Candidate]
-> (Candidate -> TCM YesNo)
-> TCM ([(Candidate, TCErr)], [(Candidate, Term)])
filterResettingState m cands f = do
ctxArgs <- getContextArgs
let ctxElims = map Apply ctxArgs
result <- mapM (\c -> do bs <- localTCStateSaving (f c); return (c, bs)) cands
-- Check that there aren't any hard failures
case [ err | (_, (HellNo err, _)) <- result ] of
err : _ -> throwError err
[] -> return ()
-- c : Candidate
-- r : YesNo
-- a : Type (fully instantiated)
-- s : TCState
let
result' = [ (c, v, s) | (c, (r, s)) <- result, v <- maybeToList (fromYes r) ]
overlap = flip all result \(c, (r, s)) -> case r of
Yes _ False -> False
_ -> True
result'' <- dropSameCandidates m overlap result'
case result'' of
[(c, v, s)] -> ([], [(c, v)]) <$ putTC s
_ -> do
let bad = [ (c, err) | (c, (NoBecause err, _)) <- result ]
good = [ (c, v) | (c, v, _) <- result'' ]
return (bad, good)
-- | The state used to reduce a list of candidates according to the
-- overlap rules.
data OverlapState item = OverlapState
{ survivingCands :: [item]
-- ^ The reduced list.
, guardingCands :: [Candidate]
-- ^ Overlapping candidates that have been discarded, which are kept
-- around because they might still discard some overlappable
-- candidates.
}
-- | Apply the instance overlap rules to reduce the list of candidates.
resolveInstanceOverlap
:: forall item.
Bool
-> Relevance
-> (item -> Candidate)
-> [item]
-> TCM [item]
resolveInstanceOverlap overlapOk rel itemC cands = wrapper where
wrapper
-- If all the candidates are incoherent: choose the leftmost candidate.
| all (isIncoherent . candidateOverlap . itemC) cands
, (c:_) <- cands = pure [c]
-- If all the candidates are record field overlap: choose the leftmost candidate.
| all ((== FieldOverlap) . candidateOverlap . itemC) cands
, (c:_) <- cands = pure [c]
-- If none of the candidates have a special overlap mode: there's no
-- reason to do any work.
| all ((DefaultOverlap ==) . candidateOverlap . itemC) cands = pure cands
| not overlapOk = pure cands
-- If some of the candidates are overlappable/overlapping, then we
-- should do the work.
| otherwise = Bench.billTo [Bench.Typing, Bench.InstanceSearch, Bench.CheckOverlap] do
reportSDoc "tc.instance.overlap" 30 $ "overlapping instances:" $$ vcat (map (debugCandidate . itemC) cands)
sinkIncoherent . survivingCands <$> foldrM insert (OverlapState [] []) cands
isGlobal Candidate{candidateKind = GlobalCandidate _} = True
isGlobal _ = False
-- At the end of the process, we might still have some incoherent and
-- non-incoherent candidates, since the user might have an instance
-- which fixes some arguments in a way that prevents it from serving
-- as a specialisation (see test/Succeed/Overlap1).
--
-- See test/Succeed/OverlapDupe for a case where this is necessary.
sinkIncoherent :: [item] -> [item]
sinkIncoherent cands = case List.partition (isIncoherent . itemC) cands of
(as, [c]) | all (isGlobal . itemC) as -> pure c
(as, cs) | all (isGlobal . itemC) as -> cs ++ as
_ -> cands
-- Insert a new item into the overlap state.
insertNew
:: OverlapState item -- The state to insert into
-> item -- The item to insert
-> [item] -- Old items which we might overlap/be overlapped by
-> TCM (OverlapState item)
insertNew oldState new [] = pure oldState{ survivingCands = [new] }
insertNew oldState newItem oldItems@(oldItem:olds) = do
let
new = itemC newItem
old = itemC oldItem
reportSDoc "tc.instance.overlap" 50 $ vcat
[ "comparing new candidate"
, nest 2 (debugCandidate new)
, "versus old candidate"
, nest 2 (debugCandidate old)
]
let
-- If the new candidate overrides the old, drop it. But if the old
-- candidate was overlapping (and the new one isn't), we keep it
-- as a guard, since it might knock out future candidates.
newold = insertNew oldState newItem olds <&> \case
OverlapState items guards ->
if not (isOverlapping new) && isOverlapping old
then OverlapState items guards
else OverlapState items (old:guards)
-- If the old candidate overrides the new, then stop inserting.
-- But if the new candidate is overlapping, it can be added as a
-- guard.
oldnew = do
if isOverlapping old || not (isOverlapping new) then pure oldState{ survivingCands = oldItems } else do
let OverlapState{ guardingCands = guards } = oldState
reportSDoc "tc.instance.overlap" 40 $ vcat
[ "will become guard:"
, nest 2 (debugCandidate new)
, "old items:"
, nest 2 (vcat (map (debugCandidate . itemC) oldItems))
]
-- But we can't /just/ add it to the list of guards: the new
-- item might conflict with some of the other old candidates.
-- We must remove those.
alive <- filterM (fmap not . doesCandidateOverlap new . itemC) oldItems
pure $ OverlapState alive (new:guards)
-- If neither overrides the other, keep both!
neither = insertNew oldState newItem olds <&> \case
OverlapState items guards -> OverlapState (oldItem:items) guards
ifM (new `doesCandidateOverlap` old)
{- then -} newold
{- else -} (ifM (old `doesCandidateOverlap` new)
{- then -} oldnew
{- else -} neither)
-- Insert a new instance into the given overlap set.
insert :: item -> OverlapState item -> TCM (OverlapState item)
insert newItem oldState@(OverlapState oldItems guards) = do
let new = itemC newItem
-- If the new candidate is overridden by any of the guards, we can
-- ditch it immediately.
guarded <- anyM (`doesCandidateOverlap` new) guards
reportSDoc "tc.instance.overlap" 40 $ vcat
[ "inserting new candidate:"
, nest 2 (debugCandidate new)
, "against old candidates"
, nest 2 (vcat (map (debugCandidate . itemC) oldItems))
, "and guarding candidates"
, nest 2 (vcat (map debugCandidate guards))
, "is guarded?" <+> prettyTCM guarded
]
if guarded then pure oldState else insertNew oldState newItem oldItems
-- Drop all candidates which are judgmentally equal to the first one.
-- This is sufficient to reduce the list to a singleton should all be equal.
dropSameCandidates :: MetaId -> Bool -> [(Candidate, Term, TCState)] -> TCM [(Candidate, Term, TCState)]
dropSameCandidates m overlapOk cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
!nextMeta <- nextLocalMeta
isRemoteMeta <- isRemoteMeta
-- Does "it" contain any fresh meta-variables?
let freshMetas = getAny . allMetas (\m -> Any (not (isRemoteMeta m || m < nextMeta)))
rel <- getRelevance <$> lookupMetaModality m
-- Take overlappable candidates into account
cands <- resolveInstanceOverlap overlapOk rel fst3 cands0
reportSDoc "tc.instance.overlap" 30 $ "instances after resolving overlap:" $$ vcat (map (debugCandidate . fst3) cands)
reportSDoc "tc.instance" 50 $ vcat
[ "valid candidates:"
, nest 2 $ vcat [ if freshMetas v then "(redacted)" else
sep [ prettyTCM v ]
| (_, v, _) <- cands ] ]
case cands of
[] -> return cands
cvd : _ | isIrrelevant rel -> do
reportSLn "tc.instance" 30 "dropSameCandidates: Meta is irrelevant so any candidate will do."
return [cvd]
-- If there's nothing, try not to reduce the candidate.
[cvd] -> pure [cvd]
cvd@(_, v, _) : vas -> do
let
equal :: (Candidate, Term, a) -> TCM Bool
equal (c, v', _)
| isIncoherent c = return True -- See 'sinkIncoherent'
| freshMetas v' = return False -- If there are fresh metas we can't compare
| otherwise =
verboseBracket "tc.instance" 30 "dropSameCandidates: " $ do
reportSDoc "tc.instance" 30 $ sep [ prettyTCM v <+> "==", nest 2 $ prettyTCM v' ]
a <- uncurry piApplyM =<< ((,) <$> getMetaType m <*> getContextArgs)
pureEqualTermB a v v' <&> \case
Left{} -> False
Right b -> b
-- If we do actually have to remove overlap then we have to reduce
-- the candidate to eliminate any "phantom" dependencies on fresh
-- metas.
v <- reduce v
if
| freshMetas v -> do
reportSLn "tc.instance" 30 "dropSameCandidates: Solution of instance meta has fresh metas so we don't filter equal candidates yet"
return (cvd : vas)
| otherwise -> (cvd :) <$> dropWhileM equal vas
data YesNo = Yes Term Bool | No | NoBecause TCErr | HellNo TCErr
deriving (Show)
fromYes :: YesNo -> Maybe Term
fromYes (Yes t _) = Just t
fromYes _ = Nothing
debugCandidate' :: MonadPretty m => Bool -> Bool -> Candidate -> m Doc
debugCandidate' raw term c@(Candidate q v t overlap) =
let
cand
| term = prettyTCM v
| otherwise = prettyTCM c
ty
| raw = nest 2 (pretty t)
| otherwise = prettyTCM t
head = fsep [ "-", pretty overlap, cand, ":" ]
in if | raw -> sep [ head, ty ]
| otherwise -> head <+> ty
debugCandidate :: MonadPretty m => Candidate -> m Doc
debugCandidate = debugCandidate' False False
debugCandidateRaw :: MonadPretty m => Candidate -> m Doc
debugCandidateRaw = debugCandidate' True False
debugCandidateTerm :: MonadPretty m => Candidate -> m Doc
debugCandidateTerm = debugCandidate' False True
-- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
-- @checkCandidates m t cands@ returns a refined list of valid candidates and
-- candidates that failed some constraints.
checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe ([(Candidate, TCErr)], [(Candidate, Term)]))
checkCandidates m t cands =
verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ "target:" <+> prettyTCM t
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ "candidates", vcat (map debugCandidate cands) ]
t <- instantiateFull t
cands'@(_, okay) <- filterResettingState m cands (checkCandidateForMeta m t)
reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
[ "valid candidates", vcat (map (debugCandidate . fst) okay) ]
reportSDoc "tc.instance.candidates" 60 $ nest 2 $ vcat
[ "valid candidates", vcat (map (debugCandidateTerm . fst) okay) ]
return cands'
where
anyMetaTypes :: [Candidate] -> TCM Bool
anyMetaTypes [] = return False
anyMetaTypes (Candidate _ _ a _ : cands) = do
a <- instantiate a
case unEl a of
MetaV{} -> return True
_ -> anyMetaTypes cands
checkDepth :: Term -> Type -> TCM YesNo -> TCM YesNo
checkDepth c a k = locallyTC eInstanceDepth succ $ do
d <- viewTC eInstanceDepth
maxDepth <- maxInstanceSearchDepth
when (d > maxDepth) $ typeError $ InstanceSearchDepthExhausted c a maxDepth
k
checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNo
checkCandidateForMeta m t (Candidate q term t' _) = checkDepth term t' $ do
Bench.billTo [Bench.Typing, Bench.InstanceSearch, Bench.FilterCandidates] $ do
whenProfile Profile.Instances $ tick "checkCandidateForMeta"
-- Andreas, 2015-02-07: New metas should be created with range of the
-- current instance meta, thus, we set the range.
mv <- lookupLocalMeta m
setCurrentRange mv $ runCandidateCheck $
verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do
reportSDoc "tc.instance" 20 $ vcat
[ "checkCandidateForMeta"
, " t =" <+> prettyTCM t
, " t' =" <+> prettyTCM t'
, " term =" <+> prettyTCM term
]
reportSDoc "tc.instance" 70 $ vcat
[ " t =" <+> pretty t
, " t' =" <+> pretty t'
, " term =" <+> pretty term
]
debugConstraints
-- Apply hidden and instance arguments (in case of
-- --overlapping-instances, this performs recursive
-- inst. search!).
(args, t'') <- implicitArgs (-1) (\h -> notVisible h) t'
reportSDoc "tc.instance" 20 $
"instance search: checking" <+> prettyTCM t'' <+> "<=" <+> prettyTCM t
reportSDoc "tc.instance" 70 $ vcat
[ "instance search: checking (raw)"
, nest 4 $ pretty t''
, nest 2 $ "<="
, nest 4 $ pretty t
]
-- Check whether this candidate is OK, and whether it is okay
-- for the overlap check. For the candidate to be acceptable,
-- its type must be a subtype of the goal type.
(cons, overlapOk) <- ifNoConstraints_ (leqType t'' t) (pure ([], True)) \pid -> do
-- To know if this candidate is safe for overlap, we have to
-- check that it does not constrain the type of the instance
-- goal. We can do this by running it in a new problem and
-- checking whether the computation produced any constraints
-- that are blocked by the instance goal.
cons <- getConstraintsForProblem pid
-- Make sure to put these constraints back if we end up
-- solving the instance goal with this candidate.
stealConstraints pid
let
blocking = foldMap (allBlockingMetas . constraintUnblocker) cons
!ok = getAll $! flip allMetas t (All . not . flip Set.member blocking)
pure (cons, ok)
debugConstraints
flip catchError (return . NoBecause) $ do
-- make a pass over constraints, to detect cases where
-- some are made unsolvable by the type comparison, but
-- don't do this for FindInstance's to prevent loops.
solveAwakeConstraints' True
-- We need instantiateFull here to remove 'local' metas
v <- instantiateFull =<< (term `applyDroppingParameters` args)
reportSDoc "tc.instance" 15 $
vcat [ sep [ ("instance search: found solution for" <+> prettyTCM m) <> ":"
, nest 2 $ prettyTCM v ]
, "app: " <+> (nest 2 $ prettyTCM =<< (term `applyDroppingParameters` args))
]
reportSDoc "tc.instance.overlap" 30 $
"candidate" <+> prettyTCM v <+> "okay for overlap?" <+> prettyTCM overlapOk
$$ vcat (map prettyTCM cons)
whenProfile Profile.Instances $ tick "checkCandidateForMeta: yes"
return $ Yes v overlapOk
where
runCandidateCheck = flip catchError handle . nowConsideringInstance
hardFailure :: TCErr -> Bool
hardFailure (TypeError _ _ err) =
case clValue err of
InstanceSearchDepthExhausted{} -> True
_ -> False
hardFailure _ = False
handle :: TCErr -> TCM YesNo
handle err
| hardFailure err = do
whenProfile Profile.Instances $ tick "checkCandidateForMeta: no"
return $ HellNo err
| otherwise = do
reportSDoc "tc.instance" 50 $ "candidate failed type check:" <+> prettyTCM err
whenProfile Profile.Instances $ tick "checkCandidateForMeta: no"
return No
nowConsideringInstance :: (ReadTCState m) => m a -> m a
nowConsideringInstance = locallyTCState stConsideringInstance $ const True
-- Rather than just the instance constraints, these are the constraints
-- which could be suspended by being under 'nowConsideringInstances',
-- which also includes unquote constraints.
isInstanceProblemConstraint :: ProblemConstraint -> Bool
isInstanceProblemConstraint c = case clValue (theConstraint c) of
FindInstance{} -> True
UnquoteTactic{} -> True
_ -> False
wakeupInstanceConstraints :: TCM ()
wakeupInstanceConstraints =
unlessM shouldPostponeInstanceSearch $ do
wakeConstraints (wakeUpWhen_ isInstanceProblemConstraint)
solveAwakeInstanceConstraints
solveAwakeInstanceConstraints :: TCM ()
solveAwakeInstanceConstraints =
solveSomeAwakeConstraints isInstanceProblemConstraint False
postponeInstanceConstraints :: TCM a -> TCM a
postponeInstanceConstraints m =
locallyTCState stPostponeInstanceSearch (const True) m <* wakeupInstanceConstraints
flushInstanceConstraints :: TCM ()
flushInstanceConstraints = locallyTCState stInstanceHack (const True) $ wakeupInstanceConstraints
-- | To preserve the invariant that a constructor is not applied to its
-- parameter arguments, we explicitly check whether function term
-- we are applying to arguments is a unapplied constructor.
-- In this case we drop the first 'conPars' arguments.
-- See Issue670a.
-- Andreas, 2013-11-07 Also do this for projections, see Issue670b.
-- Szumi, 2025-05-05: Unapplied projections are not considered by instance
-- search since #938.
applyDroppingParameters :: Term -> Args -> TCM Term
applyDroppingParameters t vs = do
let fallback = return $ t `apply` vs
case t of
Con c ci [] -> do
def <- theDef <$> getConInfo c
case def of
Constructor {conPars = n, conData = d} -> do
-- Szumi, 2025-05-05, issue #7853: don't drop parameters from the current module.
fv <- getDefFreeVars d
return $ Con c ci (map Apply $ drop (n - fv) vs)
_ -> __IMPOSSIBLE__
-- Def f [] -> do
-- -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
-- mp <- isRelevantProjection f
-- case mp of
-- Just Projection{projIndex = n} -> do
-- case drop n vs of
-- [] -> return t
-- u : us -> (`apply` us) <$> applyDef ProjPrefix f u
-- _ -> fallback
_ -> fallback
---------------------------------------------------------------------------
-- * Instance definitions
---------------------------------------------------------------------------
data OutputTypeName
= OutputTypeName QName
| OutputTypeVar
| OutputTypeVisiblePi
| OutputTypeNameNotYetKnown Blocker
| NoOutputTypeName
-- | Strips all hidden and instance Pi's and return the argument
-- telescope, the head term, and its name, if possible.
getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
-- 2023-10-26, Jesper, issue #6941: To make instance search work correctly for
-- abstract or opaque instances, we need to ignore abstract mode when computing
-- the output type name.
getOutputTypeName t = ignoreAbstractMode $ do
TelV tel t' <- telViewUpTo' (-1) notVisible t
ifBlocked (unEl t') (\b t -> return (tel , __DUMMY_TERM__, OutputTypeNameNotYetKnown b)) $ \ _ v ->
case v of
-- Possible base types:
Def n _ -> return (tel, v, OutputTypeName n)
Sort{} -> return (tel, v, NoOutputTypeName)
Var n _ -> return (tel, v, OutputTypeVar)
Pi{} -> return (tel, v, OutputTypeVisiblePi)
-- Not base types:
Con{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
MetaV{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s
-- | Register the definition with the given type as an instance.
-- Issue warnings if instance is unusable.
addTypedInstance ::
QName -- ^ Name of instance.
-> Type -- ^ Type of instance.
-> TCM ()
addTypedInstance = addTypedInstance' True False Nothing
-- | Like 'addTypedInstance', but delete any existing entries for the
-- given name from the discrimination tree.
readdTypedInstance ::
QName -- ^ Name of instance.
-> Type -- ^ Type of instance.
-> TCM ()
readdTypedInstance = addTypedInstance' True True Nothing
-- | Register the definition with the given type as an instance.
addTypedInstance'
:: Bool -- ^ Should we print warnings for unusable instance declarations?
-> Bool -- ^ Is this the second time we're adding this QName as an instance?
-> Maybe InstanceInfo -- ^ Is this instance a copy?
-> QName -- ^ Name of instance.
-> Type -- ^ Type of instance.
-> TCM ()
addTypedInstance' w readd orig inst t = do
reportSDoc "tc.instance.add" 30 $ vcat
[ "adding typed instance" <+> prettyTCM inst <+> "with type"
, prettyTCM =<< flip abstract t <$> getContextTelescope
]
(tel, hdt, n) <- getOutputTypeName t
case n of
OutputTypeName n -> addContext tel $ do
tele <- getContextTelescope
-- Insert the instance into the instance table, putting it in the
-- discrimination tree *and* bumping the total number of instances
-- for this class.
tree <- useTC stInstanceTree
-- Amélia, 2025-02-28: If the instance we're adding has no type
-- signature, we end up adding it to the tree twice: once with a
-- useless type, and once after checking the RHS (which will have
-- narrowed the type).
--
-- To avoid spurious overlap, the useful key should trump the
-- useless key, so we filter this QName out of the tree when
-- re-adding an instance.
let
tree' | readd = deleteFromDT (Set.singleton inst) tree
| otherwise = tree
tree' <- insertDT (length tele) hdt inst $! tree'
setTCLens stInstanceTree tree'
modifyTCLens' (stSignature . sigInstances . itableCounts) $
if readd then Map.insertWith (+) n 1 else id
let
info = flip fromMaybe orig InstanceInfo
{ instanceClass = n
, instanceOverlap = DefaultOverlap
}
-- This is no longer used to build the instance table for imported
-- modules, but it is still used to know if an instance should be
-- copied when applying a section.
modifySignature $ updateDefinition inst \ d -> d { defInstance = Just info }
-- If there's anything visible in the context, which will
-- eventually end up in the instance's type, let's make a note to
-- get rid of it before serialising the instance table.
con <- isConstructor inst
-- However, do note that data constructors can have "visible
-- arguments" in their global type which.. aren't actually
-- visible: the parameters.
when (any visible tele && not con) $ modifyTCLens' stTemporaryInstances $ Set.insert inst
OutputTypeNameNotYetKnown b -> do
addUnknownInstance inst
addConstraint b $ ResolveInstanceHead inst
NoOutputTypeName -> when w $ warning $ WrongInstanceDeclaration
OutputTypeVar -> when w $ warning $ WrongInstanceDeclaration
OutputTypeVisiblePi -> when w $ warning $ InstanceWithExplicitArg inst
resolveInstanceHead :: QName -> TCM ()
resolveInstanceHead q = do
clearUnknownInstance q
-- Andreas, 2022-12-04, issue #6380:
-- Do not warn about unusable instances here.
addTypedInstance' False True Nothing q =<< typeOfConst q
-- | Try to solve the instance definitions whose type is not yet known, report
-- an error if it doesn't work and return the instance table otherwise.
getInstanceDefs :: TCM InstanceTable
getInstanceDefs = do
(table, pending) <- getAllInstanceDefs
unless (null pending) $ do
patternViolation alwaysUnblock -- TODO: more refined unblocking
return table
-- | Prune an 'Interface' to remove any instances that would be
-- inapplicable in child modules.
--
-- While in a section with visible arguments, we add any instances
-- defined locally to the instance table: you have to be able to find
-- them, after all! Conservatively, all of the local variables are
-- turned into 'FlexK's, i.e., wildcards.
--
-- But when we leave such a section, these instances have no more value:
-- even though they might technically be in scope, their types are
-- malformed, since they have visible pis.
--
-- This function deletes these instances from the instance tree in the
-- given signature to save on serialisation time *and* time spent
-- checking for candidate validity in client modules. It can't do this
-- directly in the TC state to prevent these instances from going out of
-- scope before interaction (see #7196).
pruneTemporaryInstances :: Interface -> TCM Interface
pruneTemporaryInstances int = do
todo <- useTC stTemporaryInstances
reportSDoc "tc.instance.prune" 30 $ vcat
[ "leaving section"
, prettyTCM =<< getContextTelescope
, "todo:" <+> prettyTCM todo
]
let sig' = over (sigInstances . itableTree) (deleteFromDT todo) (iSignature int)
pure int{ iSignature = sig' }