idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.Unify

Documentation

match_unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] -> TC [(Name, TT Name)] Source

unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [Name] -> [FailContext] -> TC ([(Name, TT Name)], Fails) Source

type Fails = [(TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)] Source

data FailContext Source

Constructors

FailContext 

Fields

fail_sourceloc :: FC
 
fail_fn :: Name
 
fail_param :: Name
 

Instances

data FailAt Source

Constructors

Match 
Unify 

Instances

unrecoverable :: Fails -> Bool Source