Agda.TypeChecking.Rules.LHS.Unify

Documentation

type UnificationResult = UnificationResult' (Telescope, PatternSubstitution)

Result of unifyIndices.

data UnificationResult' a

Constructors

Unifies a

Unification succeeded.

NoUnify TCErr

Terms are not unifiable.

DontKnow TCErr

Some other error happened, unification got stuck.

Instances

Functor UnificationResult'

Methods

fmap :: (a -> b) -> UnificationResult' a -> UnificationResult' b

(<$) :: a -> UnificationResult' b -> UnificationResult' a

Foldable UnificationResult'

Methods

fold :: Monoid m => UnificationResult' m -> m

foldMap :: Monoid m => (a -> m) -> UnificationResult' a -> m

foldr :: (a -> b -> b) -> b -> UnificationResult' a -> b

foldr' :: (a -> b -> b) -> b -> UnificationResult' a -> b

foldl :: (b -> a -> b) -> b -> UnificationResult' a -> b

foldl' :: (b -> a -> b) -> b -> UnificationResult' a -> b

foldr1 :: (a -> a -> a) -> UnificationResult' a -> a

foldl1 :: (a -> a -> a) -> UnificationResult' a -> a

toList :: UnificationResult' a -> [a]

null :: UnificationResult' a -> Bool

length :: UnificationResult' a -> Int

elem :: Eq a => a -> UnificationResult' a -> Bool

maximum :: Ord a => UnificationResult' a -> a

minimum :: Ord a => UnificationResult' a -> a

sum :: Num a => UnificationResult' a -> a

product :: Num a => UnificationResult' a -> a

Traversable UnificationResult'

Methods

traverse :: Applicative f => (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)

sequenceA :: Applicative f => UnificationResult' (f a) -> f (UnificationResult' a)

mapM :: Monad m => (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)

sequence :: Monad m => UnificationResult' (m a) -> m (UnificationResult' a)

Show a => Show (UnificationResult' a)

Methods

showsPrec :: Int -> UnificationResult' a -> ShowS

show :: UnificationResult' a -> String

showList :: [UnificationResult' a] -> ShowS

unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult

unifyIndices_ :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm (Telescope, PatternSubstitution)

Unify indices.

In unifyIndices_ flex a us vs,

a is the type eliminated by us and vs (usally the type of a constructor), need not be reduced,

us and vs are the argument lists to unify,

flex is the set of flexible (instantiable) variabes in us and vs.

The result is the most general unifier of us and vs.