Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

Documentation

type UnificationResult = UnificationResult' (Telescope, PatternSubstitution) Source #

Result of unifyIndices.

data UnificationResult' a Source #

Constructors

Unifies a	Unification succeeded.
NoUnify TCErr	Terms are not unifiable.
DontKnow TCErr	Some other error happened, unification got stuck.

Instances

Functor UnificationResult' Source #
Methods fmap :: (a -> b) -> UnificationResult' a -> UnificationResult' b # (<$) :: a -> UnificationResult' b -> UnificationResult' a #
Foldable UnificationResult' Source #
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' Source #
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) Source #
Methods showsPrec :: Int -> UnificationResult' a -> ShowS # show :: UnificationResult' a -> String # showList :: [UnificationResult' a] -> ShowS #

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

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

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.