Agda.TypeChecking.Injectivity

Injectivity, or more precisely, "constructor headedness", is a property of functions defined by pattern matching that helps us solve constraints involving blocked applications of such functions. Blocked shall mean here that pattern matching is blocked on a meta variable, and constructor headedness lets us learn more about that meta variable.

Consider the simple example: isZero : Nat -> Bool isZero zero = true isZero (suc n) = false This function is constructor-headed, meaning that all rhss are headed by a distinct constructor. Thus, on a constraint like isZero ?X = false : Bool involving an application of isZero that is blocked on meta variable ?X, we can exploit injectivity and learn that ?X = suc ?Y for a new meta-variable ?Y.

Which functions qualify for injectivity?

1. The function needs to have at least one non-absurd clause that has a proper match, meaning that the function can actually be blocked on a meta. Proper matches are these patterns:

• data constructor (ConP, but not record constructor)
• literal (LitP)
• HIT-patterns (DefP)

Projection patterns (ProjP) are excluded because metas cannot occupy their place!

2. All the clauses that satisfy (1.) need to be headed by a distinct constructor.

Documentation

headSymbol :: Term -> TCM (Maybe TermHead)

isUnstableDef :: PureTCM m => QName -> m Bool

Is this a matchable definition, or constructor, which reduces based on interval substitutions?

headSymbol' :: (PureTCM m, MonadError TCErr m) => Term -> m (Maybe TermHead)

Do a full whnf and treat neutral terms as rigid. Used on the arguments to an injective functions and to the right-hand side. Only returns heads which are stable under interval substitution, i.e. NOT path constructors or generated hcomp/transp!

topLevelArg :: Clause -> Int -> Maybe TermHead

Does deBruijn variable i correspond to a top-level argument, and if so which one (index from the left).

joinHeadMaps :: [InversionMap c] -> InversionMap c

Join a list of inversion maps.

updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c)

Update the heads of an inversion map.

checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse

checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse

Precondition: all the given clauses are non-absurd and contain a proper match.

checkOverapplication :: HasConstInfo m => Elims -> InversionMap Clause -> m (InversionMap Clause)

If a clause is over-applied we can't trust the head (Issue 2944). For instance, the clause might be `f ps = u , v` and the actual call `f vs .fst`. In this case the head will be the head of u rather than `_,_`.

instantiateVarHeads :: (PureTCM m, MonadError TCErr m) => QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))

Turn variable heads, referring to top-level argument positions, into proper heads. These might still be VarHead, but in that case they refer to deBruijn variables. Checks that the instantiated heads are still rigid and distinct.

functionInverse :: (PureTCM m, MonadError TCErr m) => Term -> m InvView

Argument should be in weak head normal form.

data InvView

Constructors

Inv QName [Elim] (InversionMap Clause)

NoInv

useInjectivity :: MonadConversion m => CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()

Precondition: The first term must be blocked on the given meta and the second must be neutral.

invertFunction :: MonadConversion m => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m ()

The second argument should be a blocked application and the third argument the inverse of the applied function.

forcePiUsingInjectivity :: Type -> TCM Type