{-|
Module      : Idris.Core.Unify
Description : Idris' unification code.

License     : BSD3
Maintainer  : The Idris Community.

Unification is applied inside the theorem prover. We're looking for holes
which can be filled in, by matching one term's normal form against another.
Returns a list of hole names paired with the term which solves them, and
a list of things which need to be injective.

-}
{-# LANGUAGE FlexibleContexts, PatternGuards #-}

module Idris.Core.Unify(
    match_unify, unify
  , Fails, FailContext(..), FailAt(..)
  , unrecoverable
  ) where

import Idris.Core.Evaluate
import Idris.Core.TT

import Control.Monad.State.Strict
import Data.List
import Data.Maybe

-- terms which need to be injective, with the things we're trying to unify
-- at the time
data FailAt = Match | Unify
     deriving (Int -> FailAt -> ShowS
[FailAt] -> ShowS
FailAt -> String
(Int -> FailAt -> ShowS)
-> (FailAt -> String) -> ([FailAt] -> ShowS) -> Show FailAt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FailAt -> ShowS
showsPrec :: Int -> FailAt -> ShowS
$cshow :: FailAt -> String
show :: FailAt -> String
$cshowList :: [FailAt] -> ShowS
showList :: [FailAt] -> ShowS
Show, FailAt -> FailAt -> Bool
(FailAt -> FailAt -> Bool)
-> (FailAt -> FailAt -> Bool) -> Eq FailAt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FailAt -> FailAt -> Bool
== :: FailAt -> FailAt -> Bool
$c/= :: FailAt -> FailAt -> Bool
/= :: FailAt -> FailAt -> Bool
Eq)

data FailContext = FailContext { FailContext -> FC
fail_sourceloc :: FC,
                                 FailContext -> Name
fail_fn        :: Name,
                                 FailContext -> Name
fail_param     :: Name
                               }
  deriving (FailContext -> FailContext -> Bool
(FailContext -> FailContext -> Bool)
-> (FailContext -> FailContext -> Bool) -> Eq FailContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FailContext -> FailContext -> Bool
== :: FailContext -> FailContext -> Bool
$c/= :: FailContext -> FailContext -> Bool
/= :: FailContext -> FailContext -> Bool
Eq, Int -> FailContext -> ShowS
[FailContext] -> ShowS
FailContext -> String
(Int -> FailContext -> ShowS)
-> (FailContext -> String)
-> ([FailContext] -> ShowS)
-> Show FailContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FailContext -> ShowS
showsPrec :: Int -> FailContext -> ShowS
$cshow :: FailContext -> String
show :: FailContext -> String
$cshowList :: [FailContext] -> ShowS
showList :: [FailContext] -> ShowS
Show)

type Fails = [(TT Name, TT Name, -- unification error
               Bool, -- ready to retry yet
               Env, Err, [FailContext], FailAt)]

unrecoverable :: Fails -> Bool
unrecoverable :: Fails -> Bool
unrecoverable = ((TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt) -> Bool)
-> Fails -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt) -> Bool
forall {a} {b} {c} {d} {t} {f} {g}.
(a, b, c, d, Err' t, f, g) -> Bool
bad
  where bad :: (a, b, c, d, Err' t, f, g) -> Bool
bad (a
_,b
_,c
_,d
_, Err' t
err, f
_, g
_) = Err' t -> Bool
forall {t}. Err' t -> Bool
unrec Err' t
err

        unrec :: Err' t -> Bool
unrec (CantUnify Bool
r (t, Maybe Provenance)
_ (t, Maybe Provenance)
_ Err' t
_ [(Name, t)]
_ Int
_) = Bool -> Bool
not Bool
r
        unrec (At FC
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec (Elaborating String
_ Name
_ Maybe t
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec Err' t
_ = Bool
False

data UInfo = UI Int Fails
     deriving Int -> UInfo -> ShowS
[UInfo] -> ShowS
UInfo -> String
(Int -> UInfo -> ShowS)
-> (UInfo -> String) -> ([UInfo] -> ShowS) -> Show UInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UInfo -> ShowS
showsPrec :: Int -> UInfo -> ShowS
$cshow :: UInfo -> String
show :: UInfo -> String
$cshowList :: [UInfo] -> ShowS
showList :: [UInfo] -> ShowS
Show

-- | Smart constructor for unification errors that takes into account the FailContext
cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
cantUnify :: forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [] Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i = Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i
cantUnify (FailContext FC
fc Name
f Name
x : [FailContext]
prev) Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i =
  FC -> Err' t -> Err' t
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
forall t. Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ElaboratingArg Name
f Name
x
          ((FailContext -> (Name, Name)) -> [FailContext] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FailContext FC
_ Name
f' Name
x') -> (Name
f', Name
x')) [FailContext]
prev)
          (Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i))

-- Solve metavariables by matching terms against each other
-- Not really unification, of course!

match_unify :: Context -> Env ->
               (TT Name, Maybe Provenance) ->
               (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
               TC [(Name, TT Name)]
match_unify :: Context
-> Env
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, TT Name)]
match_unify Context
ctxt Env
env (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [Name]
inj [Name]
holes [FailContext]
from =
     case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topx)
                           (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topy)) (Int -> Fails -> UInfo
UI Int
0 []) of
        OK ([(Name, TT Name)]
v, UI Int
_ []) ->
           do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall {a} {r}.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
              [(Name, TT Name)] -> TC [(Name, TT Name)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall {a}. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
        TC ([(Name, TT Name)], UInfo)
res ->
               let topxn :: TT Name
topxn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topx)
                   topyn :: TT Name
topyn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topy) in
                     case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] TT Name
topxn TT Name
topyn)
                                (Int -> Fails -> UInfo
UI Int
0 []) of
                       OK ([(Name, TT Name)]
v, UI Int
_ Fails
fails) ->
                            do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall {a} {r}.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
                               [(Name, TT Name)] -> TC [(Name, TT Name)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall {a}. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
                       Error Err
e ->
                        -- just normalise the term we're matching against
                         case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] TT Name
topxn TT Name
topy)
                                  (Int -> Fails -> UInfo
UI Int
0 []) of
                           OK ([(Name, TT Name)]
v, UI Int
_ Fails
fails) ->
                              do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall {a} {r}.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
                                 [(Name, TT Name)] -> TC [(Name, TT Name)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall {a}. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
                           TC ([(Name, TT Name)], UInfo)
_ -> Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
e
  where
    un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
          StateT UInfo
          TC [(Name, TT Name)]

    un :: [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
names tx :: TT Name
tx@(P NameType
_ Name
x TT Name
_) TT Name
tm
        | TT Name
tx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
tm Bool -> Bool -> Bool
&& Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
            = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState UInfo (t TC)) =>
[((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
names TT Name
tx (Name
x, TT Name
tm)
    un [((Name, Name), TT Name)]
names TT Name
tm ty :: TT Name
ty@(P NameType
_ Name
y TT Name
_)
        | TT Name
ty TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
tm Bool -> Bool -> Bool
&& Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
            = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *}.
(MonadTrans t, MonadState UInfo (t TC)) =>
[((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
names TT Name
ty (Name
y, TT Name
tm)
    un [((Name, Name), TT Name)]
bnames (V Int
i) (P NameType
_ Name
x TT Name
_)
        | [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
          (Name, Name) -> Name
forall a b. (a, b) -> a
fst (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
          (Name, Name) -> Name
forall a b. (a, b) -> b
snd (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un [((Name, Name), TT Name)]
bnames (P NameType
_ Name
x TT Name
_) (V Int
i)
        | [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
          (Name, Name) -> Name
forall a b. (a, b) -> a
fst (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
          (Name, Name) -> Name
forall a b. (a, b) -> b
snd (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un [((Name, Name), TT Name)]
bnames (Bind Name
x Binder (TT Name)
bx TT Name
sx) (Bind Name
y Binder (TT Name)
by TT Name
sy) | Binder (TT Name) -> Bool
forall {b}. Binder b -> Bool
notHole Binder (TT Name)
bx Bool -> Bool -> Bool
&& Binder (TT Name) -> Bool
forall {b}. Binder b -> Bool
notHole Binder (TT Name)
by
        = do [(Name, TT Name)]
h1 <- [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB [((Name, Name), TT Name)]
bnames Binder (TT Name)
bx Binder (TT Name)
by
             [(Name, TT Name)]
h2 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un (((Name
x, Name
y), Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
bx) ((Name, Name), TT Name)
-> [((Name, Name), TT Name)] -> [((Name, Name), TT Name)]
forall a. a -> [a] -> [a]
: [((Name, Name), TT Name)]
bnames) TT Name
sx TT Name
sy
             [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
    un [((Name, Name), TT Name)]
names (App AppStatus Name
_ TT Name
fx TT Name
ax) (App AppStatus Name
_ TT Name
fy TT Name
ay)
        = do [(Name, TT Name)]
hf <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
names TT Name
fx TT Name
fy
             [(Name, TT Name)]
ha <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
names TT Name
ax TT Name
ay
             [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
names [(Name, TT Name)]
hf [(Name, TT Name)]
ha
    un [((Name, Name), TT Name)]
names TT Name
x TT Name
y
        | OK Bool
True <- Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
holes TT Name
x TT Name
y = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                         let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
                                             (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
                         let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
                                     (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                         if (Bool -> Bool
not Bool
r) then TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
err
                           else do UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                                   TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
err


    uB :: [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB [((Name, Name), TT Name)]
bnames (Let RigCount
_ TT Name
tx TT Name
vx) (Let RigCount
_ TT Name
ty TT Name
vy)
         = do [(Name, TT Name)]
h1 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
              [(Name, TT Name)]
h2 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
              [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
    uB [((Name, Name), TT Name)]
bnames (Lam RigCount
_ TT Name
tx) (Lam RigCount
_ TT Name
ty) = [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB [((Name, Name), TT Name)]
bnames (Pi RigCount
r Maybe ImplicitInfo
i TT Name
tx TT Name
_) (Pi RigCount
r' Maybe ImplicitInfo
i' TT Name
ty TT Name
_) = [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB [((Name, Name), TT Name)]
bnames Binder (TT Name)
x Binder (TT Name)
y = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                       let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x))
                                           (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y))
                       let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                   (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Maybe Provenance
forall a. Maybe a
Nothing)
                                                (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s)
                                   (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                       UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y,
                                   Bool
False,
                                   Env
env, Err
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    notHole :: Binder b -> Bool
notHole (Hole b
_) = Bool
False
    notHole Binder b
_ = Bool
True

    -- TODO: there's an annoying amount of repetition between this and the
    -- main unification function. Consider lifting it out.
    -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721

    sc :: Int -> m ()
sc Int
i = do UI Int
s Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
              UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI (Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) Fails
f)

    unifyFail :: TT Name -> TT Name -> t TC b
unifyFail TT Name
x TT Name
y = do UI Int
s Fails
f <- t TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                       let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
                                           (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
                       let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
                                   (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                   (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                       UInfo -> t TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       TC b -> t TC b
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err -> TC b
forall a. Err -> TC a
tfail Err
err
    combine :: [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
    combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ((Name
n, TT Name
t) : [(Name, TT Name)]
bs)
        = case Name -> [(Name, TT Name)] -> Maybe (TT Name)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, TT Name)]
as of
            Maybe (TT Name)
Nothing -> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames ([(Name, TT Name)]
as [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name
n,TT Name
t)]) [(Name, TT Name)]
bs
            Just TT Name
t' -> do [(Name, TT Name)]
ns <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
t TT Name
t'
                          let ns' :: [(Name, TT Name)]
ns' = ((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
x, TT Name
_) -> Name
xName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n) [(Name, TT Name)]
ns
                          Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                          [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ([(Name, TT Name)]
ns' [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)]
bs)

--     substN n tm (var, sol) = (var, subst n tm sol)

    checkCycle :: [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
x' TT Name
_) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
_ TT Name
_) = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
    checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm (Name
x, TT Name
tm)
        | Context -> Name -> TT Name -> Bool
conGuarded Context
ctxt Name
x TT Name
tm = TC [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> t TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err
forall t. Name -> t -> [(Name, t)] -> Err' t
InfiniteUnify Name
x TT Name
tm (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env))
        | Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TT Name -> [Name]
forall n. Eq n => TT n -> [n]
freeNames TT Name
tm = TT Name -> TT Name -> t TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
xtm TT Name
tm
        | Bool
otherwise = [((Name, Name), TT Name)]
-> (Name, TT Name) -> t TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {a}.
(MonadTrans t, Monad (t TC)) =>
[((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (Name
x, TT Name
tm)

    checkScope :: [((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) =
        let v :: Int
v = Int -> TT Name -> Int
highV (-Int
1) TT Name
tm in
            if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
ns
               then TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"SCOPE ERROR")
               else [(a, TT Name)] -> t TC [(a, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(a
x, Int -> [((Name, Name), TT Name)] -> TT Name -> TT Name
forall {n}. Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
v [((Name, Name), TT Name)]
ns TT Name
tm)]

    bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
i [((n, n), TT n)]
ns TT n
tm
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = TT n
tm
      | Bool
otherwise = let ((n
x,n
y),TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i in
                        AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
forall n. AppStatus n
MaybeHoles (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
y (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT n
ty) (Int -> [((n, n), TT n)] -> TT n -> TT n
bind (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [((n, n), TT n)]
ns TT n
tm))
                            (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
x TT n
ty)

renameBinders :: Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env (a
x, TT Name
t) = (a
x, Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
t)

renameBindersTm :: Env -> TT Name -> TT Name
renameBindersTm :: Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
tm = [Name] -> TT Name -> TT Name
uniqueBinders (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) TT Name
tm
  where
    uniqueBinders :: [Name] -> TT Name -> TT Name
uniqueBinders [Name]
env (Bind Name
n Binder (TT Name)
b TT Name
sc)
        | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
env
             = let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
env in
                   TT Name -> TT Name
forall {n}. TT n -> TT n
explicitHole (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env) Binder (TT Name)
b)
                           ([Name] -> TT Name -> TT Name
uniqueBinders (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) (Name -> Name -> TT Name -> TT Name
forall {t}. Eq t => t -> t -> TT t -> TT t
rename Name
n Name
n' TT Name
sc))
        | Bool
otherwise = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
uniqueBinders (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env)) Binder (TT Name)
b)
                             ([Name] -> TT Name -> TT Name
uniqueBinders (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) TT Name
sc)
    uniqueBinders [Name]
env (App AppStatus Name
s TT Name
f TT Name
a) = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env TT Name
f) ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env TT Name
a)
    uniqueBinders [Name]
env TT Name
t = TT Name
t

    rename :: t -> t -> TT t -> TT t
rename t
n t
n' (P NameType
nt t
x TT t
ty) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x = NameType -> t -> TT t -> TT t
forall n. NameType -> n -> TT n -> TT n
P NameType
nt t
n' TT t
ty
    rename t
n t
n' (Bind t
x Binder (TT t)
b TT t
sc) = t -> Binder (TT t) -> TT t -> TT t
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind t
x ((TT t -> TT t) -> Binder (TT t) -> Binder (TT t)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> t -> TT t -> TT t
rename t
n t
n') Binder (TT t)
b) (t -> t -> TT t -> TT t
rename t
n t
n' TT t
sc)
    rename t
n t
n' (App AppStatus t
s TT t
f TT t
a) = AppStatus t -> TT t -> TT t -> TT t
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus t
s (t -> t -> TT t -> TT t
rename t
n t
n' TT t
f) (t -> t -> TT t -> TT t
rename t
n t
n' TT t
a)
    rename t
n t
n' TT t
t = TT t
t

    explicitHole :: TT n -> TT n
explicitHole (Bind n
n (Hole TT n
ty) TT n
sc)
       = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> Binder (TT n)
forall b. b -> Binder b
Hole TT n
ty) (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
ty) TT n
sc)
    explicitHole TT n
t = TT n
t

trimSolutions :: (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from [(Name, r, Binder (TT Name))]
env [(a, TT a)]
topns = [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
forall {a}. Eq a => [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [] ([(a, TT a)] -> [(a, TT a)]
forall {a}. Eq a => [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
topns)
  where dropPairs :: [(a, TT a)] -> [(a, TT a)]
dropPairs [] = []
        dropPairs (n :: (a, TT a)
n@(a
x, P NameType
_ a
x' TT a
_) : [(a, TT a)]
ns)
          | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' = [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
ns
          | Bool
otherwise
            = (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)] -> [(a, TT a)]
dropPairs
                    (((a, TT a) -> Bool) -> [(a, TT a)] -> [(a, TT a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a, TT a)
t -> case (a, TT a)
t of
                                      (a
n, P NameType
_ a
n' TT a
_) -> Bool -> Bool
not (a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' Bool -> Bool -> Bool
&& a
n' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x)
                                      (a, TT a)
_ -> Bool
True) [(a, TT a)]
ns)
        dropPairs ((a, TT a)
n : [(a, TT a)]
ns) = (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
ns

        followSols :: [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [(a, a)]
vs [] = [(a, TT a)] -> TC [(a, TT a)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        followSols [(a, a)]
vs ((a
n, P NameType
_ a
t TT a
_) : [(a, TT a)]
ns)
          | Just TT a
t' <- a -> [(a, TT a)] -> Maybe (TT a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
t [(a, TT a)]
ns
              = do [(a, a)]
vs' <- case TT a
t' of
                     P NameType
_ a
tn TT a
_ ->
                           if (a
n, a
tn) (a, a) -> [(a, a)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
vs then -- cycle
                                   Err -> TC [(a, a)]
forall a. Err -> TC a
tfail ([FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
False (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                            (String -> Err
forall t. String -> Err' t
Msg String
"") ([(Name, r, Binder (TT Name))] -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv [(Name, r, Binder (TT Name))]
env) Int
0)
                                   else [(a, a)] -> TC [(a, a)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
n, a
tn) (a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
: [(a, a)]
vs)
                     TT a
_ -> [(a, a)] -> TC [(a, a)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, a)]
vs
                   [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [(a, a)]
vs' ((a
n, TT a
t') (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)]
ns)
        followSols [(a, a)]
vs ((a, TT a)
n : [(a, TT a)]
ns) = do [(a, TT a)]
ns' <- [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [(a, a)]
vs [(a, TT a)]
ns
                                    [(a, TT a)] -> TC [(a, TT a)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, TT a)] -> TC [(a, TT a)]) -> [(a, TT a)] -> TC [(a, TT a)]
forall a b. (a -> b) -> a -> b
$ (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)]
ns'

unify :: Context -> Env ->
         (TT Name, Maybe Provenance) ->
         (TT Name, Maybe Provenance) ->
         [Name] -> [Name] -> [Name] -> [FailContext] ->
         TC ([(Name, TT Name)], Fails)
unify :: Context
-> Env
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, TT Name)], Fails)
unify Context
ctxt Env
env (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [Name]
inj [Name]
holes [Name]
usersupp [FailContext]
from =
--      traceWhen (hasv topx || hasv topy)
--           ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
             -- don't bother if topx and topy are different at the head
      case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un Bool
False [] (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topx)
                                  (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topy)) (Int -> Fails -> UInfo
UI Int
0 []) of
        OK ([(Name, TT Name)]
v, UI Int
_ []) -> do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall {a} {r}.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
                              ([(Name, TT Name)], Fails) -> TC ([(Name, TT Name)], Fails)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall {a}. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v', [])
        TC ([(Name, TT Name)], UInfo)
res ->
               let topxn :: TT Name
topxn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topx)
                   topyn :: TT Name
topyn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topy) in
--                     trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $
                     case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un Bool
False [] TT Name
topxn TT Name
topyn)
                                (Int -> Fails -> UInfo
UI Int
0 []) of
                       OK ([(Name, TT Name)]
v, UI Int
_ Fails
fails) ->
                            do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall {a} {r}.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
--                                trace ("OK " ++ show (topxn, topyn, v, holes)) $
                               ([(Name, TT Name)], Fails) -> TC ([(Name, TT Name)], Fails)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall {a}. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v', Fails -> Fails
forall a. [a] -> [a]
reverse Fails
fails)
--         Error e@(CantUnify False _ _ _ _ _)  -> tfail e
                       Error Err
e -> Err -> TC ([(Name, TT Name)], Fails)
forall a. Err -> TC a
tfail Err
e
  where
    injective :: TT n -> Bool
injective (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) = Bool
True
    injective (P (TCon Int
_ Int
_) n
_ TT n
_) = Bool
True
--     injective (P Ref n _)
--          | Just i <- lookupInjectiveExact n ctxt = i
    injective (App AppStatus n
_ TT n
f TT n
a)        = TT n -> Bool
injective TT n
f -- && injective a
    injective TT n
_                  = Bool
False

--     injectiveTC (P Ref n _) (P Ref n' _)
--          | Just i <- lookupInjectiveExact n ctxt,
--            n == n' = i
--     injectiveTC (App _ f a) (App _ f' a') = injectiveTC f a
--     injectiveTC _ _ = False

--     injectiveVar (P _ (MN _ _) _) = True -- TMP HACK
    injectiveVar :: TT Name -> Bool
injectiveVar (P NameType
_ Name
n TT Name
_)        = Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj
    injectiveVar (App AppStatus Name
_ TT Name
f TT Name
a)      = TT Name -> Bool
injectiveVar TT Name
f -- && injective a
    injectiveVar TT Name
_ = Bool
False

    injectiveApp :: TT Name -> Bool
injectiveApp TT Name
x = TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
x Bool -> Bool -> Bool
|| TT Name -> Bool
injectiveVar TT Name
x

    notP :: TT n -> Bool
notP (P NameType
_ n
_ TT n
_) = Bool
False
    notP TT n
_ = Bool
True

    sc :: Int -> m ()
sc Int
i = do UI Int
s Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
              UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI (Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) Fails
f)

    uplus :: m b -> m b -> m b
uplus m b
u1 m b
u2 = do UI Int
s Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                     b
r <- m b
u1
                     UI Int
s Fails
f' <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                     if (Fails -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Fails -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f')
                        then b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return b
r
                        else do UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s Fails
f); m b
u2

    un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
          StateT UInfo
          TC [(Name, TT Name)]
    un :: Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env

    un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
           StateT UInfo
           TC [(Name, TT Name)]
    un' :: Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
fn [((Name, Name), TT Name)]
names TT Name
x TT Name
y | TT Name
x TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
y = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- shortcut
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) topy :: TT Name
topy@(P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_)
                | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
                | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
                = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_)
                = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Constant Const
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
                = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(Constant Const
_)
                = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames tx :: TT Name
tx@(P NameType
_ Name
x TT Name
_) ty :: TT Name
ty@(P NameType
_ Name
y TT Name
_)
        | (Name
x,Name
y) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames Bool -> Bool -> Bool
|| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
tx Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
             = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tx TT Name
ty
        | TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
ty Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
             = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tx TT Name
ty
        -- pick the one bound earliest if both are holes
        | TT Name
tx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
ty Bool -> Bool -> Bool
&& (Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
                   Bool -> Bool -> Bool
&& (Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
            = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Name -> Env -> Integer
forall {t} {t} {b} {c}. (Eq t, Num t) => t -> t -> [(t, b, c)] -> t
envPos Integer
0 Name
x Env
env) (Integer -> Name -> Env -> Integer
forall {t} {t} {b} {c}. (Eq t, Num t) => t -> t -> [(t, b, c)] -> t
envPos Integer
0 Name
y Env
env) of
                   Ordering
LT -> do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
tx (Name
x, TT Name
ty)
                   Ordering
_ -> do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ty (Name
y, TT Name
tx)
       where envPos :: t -> t -> [(t, b, c)] -> t
envPos t
i t
n ((t
n',b
_,c
_):[(t, b, c)]
env) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
n' = t
i
             envPos t
i t
n ((t, b, c)
_:[(t, b, c)]
env) = t -> t -> [(t, b, c)] -> t
envPos (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) t
n [(t, b, c)]
env
             envPos t
_ t
_ [(t, b, c)]
_ = t
100000
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames xtm :: TT Name
xtm@(P NameType
_ Name
x TT Name
_) TT Name
tm
        | TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
                       = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                            -- injectivity check
                            [(Name, TT Name)]
x <- [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
xtm (Name
x, TT Name
tm)
                            if (TT Name -> Bool
forall {n}. TT n -> Bool
notP TT Name
tm Bool -> Bool -> Bool
&& Bool
fn)
--                               trace (show (x, tm, normalise ctxt env tm)) $
--                                 put (UI s ((tm, topx, topy) : i) f)
                                 then TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
                                 else do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                                         [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
x
        | TT Name -> Bool
pureTerm TT Name
tm, Bool -> Bool
not (TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
xtm) Bool -> Bool -> Bool
&& TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
tm
                       = do [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
xtm (Name
x, TT Name
tm)
                            TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
tm ytm :: TT Name
ytm@(P NameType
_ Name
y TT Name
_)
        | TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
                       = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                            -- injectivity check
                            [(Name, TT Name)]
x <- [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ytm (Name
y, TT Name
tm)
                            if (TT Name -> Bool
forall {n}. TT n -> Bool
notP TT Name
tm Bool -> Bool -> Bool
&& Bool
fn)
--                               trace (show (y, tm, normalise ctxt env tm)) $
--                                 put (UI s ((tm, topx, topy) : i) f)
                                 then TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tm TT Name
ytm
                                 else do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                                         [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
x
        | TT Name -> Bool
pureTerm TT Name
tm, Bool -> Bool
not (TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
ytm) Bool -> Bool -> Bool
&& TT Name -> Bool
forall {n}. TT n -> Bool
injective TT Name
tm
                       = do [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ytm (Name
y, TT Name
tm)
                            TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tm TT Name
ytm
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (V Int
i) (P NameType
_ Name
x TT Name
_)
        | [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
          (Name, Name) -> Name
forall a b. (a, b) -> a
fst (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
          (Name, Name) -> Name
forall a b. (a, b) -> b
snd (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (P NameType
_ Name
x TT Name
_) (V Int
i)
        | [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
          (Name, Name) -> Name
forall a b. (a, b) -> a
fst (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
          (Name, Name) -> Name
forall a b. (a, b) -> b
snd (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Bind Name
n (Hole TT Name
t) TT Name
sc) TT Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
topx TT Name
y
    un' Env
env Bool
fn [((Name, Name), TT Name)]
names TT Name
x topy :: TT Name
topy@(Bind Name
n (Hole TT Name
t) TT Name
sc) = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
x TT Name
topy

-- Pattern unification rule
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
tm app :: TT Name
app@(App AppStatus Name
_ TT Name
_ TT Name
_)
        | (mvtm :: TT Name
mvtm@(P NameType
_ Name
mv TT Name
_), [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
app,
          Env -> Name -> Bool
holeIn Env
env Name
mv Bool -> Bool -> Bool
|| Name
mv Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes,
          (TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TT Name -> Bool
rigid [TT Name]
args,
          [Name] -> [Int] -> TT Name -> Bool
forall {t :: * -> *}.
Foldable t =>
t Name -> [Int] -> TT Name -> Bool
containsOnly ((TT Name -> Maybe Name) -> [TT Name] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TT Name -> Maybe Name
forall {a}. TT a -> Maybe a
getname [TT Name]
args) ((TT Name -> Maybe Int) -> [TT Name] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TT Name -> Maybe Int
forall {n}. TT n -> Maybe Int
getV [TT Name]
args) TT Name
tm
          -- && TODO: tm does not refer to any variables other than those
          -- in 'args'
        = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
          [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
mvtm (Name
mv, [(Name, RigCount, TT Name)] -> TT Name -> TT Name
forall {a}. Eq a => [(a, RigCount, TT a)] -> TT a -> TT a
eta [] (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ [TT Name] -> TT Name -> TT Name
bindLams [TT Name]
args (Env -> TT Name -> TT Name
forall {n} {b}. [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv Env
env TT Name
tm))
      where rigid :: TT Name -> Bool
rigid (V Int
i) = Bool
True
            rigid (P NameType
_ Name
t TT Name
_) = Name
t Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env Bool -> Bool -> Bool
&&
                              Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
t Bool -> Bool -> Bool
|| Name
t Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
            rigid TT Name
_ = Bool
False

            getV :: TT n -> Maybe Int
getV (V Int
i) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
            getV TT n
_ = Maybe Int
forall a. Maybe a
Nothing

            getname :: TT a -> Maybe a
getname (P NameType
_ a
n TT a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
            getname TT a
_ = Maybe a
forall a. Maybe a
Nothing

            containsOnly :: t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs (V Int
i) = Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
vs
            containsOnly t Name
args [Int]
vs (P NameType
Bound Name
n TT Name
ty)
                   = Name
n Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
args Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
            containsOnly t Name
args [Int]
vs (P NameType
_ Name
n TT Name
ty)
                   = Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
n Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
                        Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
            containsOnly t Name
args [Int]
vs (App AppStatus Name
_ TT Name
f TT Name
a)
                   = t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
f Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
a
            containsOnly t Name
args [Int]
vs (Bind Name
_ Binder (TT Name)
b TT Name
sc)
                   = t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) Bool -> Bool -> Bool
&&
                     t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Int]
vs) TT Name
sc
            containsOnly t Name
args [Int]
vs TT Name
_ = Bool
True

            bindLams :: [TT Name] -> TT Name -> TT Name
bindLams [] TT Name
tm = TT Name
tm
            bindLams (TT Name
a : [TT Name]
as) TT Name
tm = TT Name -> TT Name -> TT Name
bindLam TT Name
a ([TT Name] -> TT Name -> TT Name
bindLams [TT Name]
as TT Name
tm)

            bindLam :: TT Name -> TT Name -> TT Name
bindLam (V Int
i) TT Name
tm = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind ((Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (Env
env Env -> Int -> (Name, RigCount, Binder (TT Name))
forall a. HasCallStack => [a] -> Int -> a
!! Int
i))
                                    (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy ((Name, RigCount, Binder (TT Name)) -> Binder (TT Name)
forall {a} {b} {c}. (a, b, c) -> c
sndEnv (Env
env Env -> Int -> (Name, RigCount, Binder (TT Name))
forall a. HasCallStack => [a] -> Int -> a
!! Int
i))))
                                    TT Name
tm
            bindLam (P NameType
_ Name
n TT Name
ty) TT Name
tm = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
tm
            bindLam TT Name
_ TT Name
tm = String -> TT Name
forall a. HasCallStack => String -> a
error String
"Can't happen [non rigid bindLam]"

            substEnv :: [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [] TT n
tm = TT n
tm
            substEnv ((n
n, b
_, Binder (TT n)
t) : [(n, b, Binder (TT n))]
env) TT n
tm
                = [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [(n, b, Binder (TT n))]
env (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
substV (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
t)) TT n
tm)

            -- remove any unnecessary lambdas (helps with interface
            -- resolution later).
            eta :: [(a, RigCount, TT a)] -> TT a -> TT a
eta [(a, RigCount, TT a)]
ks (Bind a
n (Lam RigCount
r TT a
ty) TT a
sc) = [(a, RigCount, TT a)] -> TT a -> TT a
eta ((a
n, RigCount
r, TT a
ty) (a, RigCount, TT a)
-> [(a, RigCount, TT a)] -> [(a, RigCount, TT a)]
forall a. a -> [a] -> [a]
: [(a, RigCount, TT a)]
ks) TT a
sc
            eta [(a, RigCount, TT a)]
ks TT a
t = [(a, RigCount, TT a)] -> TT a -> TT a
rebind [(a, RigCount, TT a)]
ks TT a
t

            rebind :: [(a, RigCount, TT a)] -> TT a -> TT a
rebind ((a
n, RigCount
r, TT a
ty) : [(a, RigCount, TT a)]
ks) (App AppStatus a
_ TT a
f (P NameType
_ a
n' TT a
_))
                | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n' = [(a, RigCount, TT a)] -> TT a -> TT a
eta [(a, RigCount, TT a)]
ks TT a
f
            rebind ((a
n, RigCount
r, TT a
ty) : [(a, RigCount, TT a)]
ks) TT a
t = [(a, RigCount, TT a)] -> TT a -> TT a
rebind [(a, RigCount, TT a)]
ks (a -> Binder (TT a) -> TT a -> TT a
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind a
n (RigCount -> TT a -> Binder (TT a)
forall b. RigCount -> b -> Binder b
Lam RigCount
r TT a
ty) TT a
t)
            rebind [(a, RigCount, TT a)]
_ TT a
t = TT a
t

    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App AppStatus Name
_ TT Name
_ TT Name
_) appy :: TT Name
appy@(App AppStatus Name
_ TT Name
_ TT Name
_)
        = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
forall {p}.
Env
-> p
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
unApp Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
appx TT Name
appy
--         = uplus (unApp fn bnames appx appy)
--                 (unifyTmpFail appx appy) -- take the whole lot

    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (P NameType
Bound Name
n' TT Name
_)))
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (P NameType
Bound Name
n' TT Name
_))) TT Name
y
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (V Int
0)))
        = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (V Int
0))) TT Name
y
        = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
--     un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
--         = un' env False ((x,y):bnames) sx sy
--     un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
--         = un' env False ((x,y):bnames) sx sy

    -- f D unifies with t -> D. This is dubious, but it helps with
    -- interface resolution for interfaces over functions.

    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (App AppStatus Name
_ TT Name
f TT Name
x) (Bind Name
n (Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) TT Name
y)
      | Name -> TT Name -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence Name
n TT Name
y Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
f
        = do [(Name, TT Name)]
ux <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
             [(Name, TT Name)]
uf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
f (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (Int -> String -> Name
sMN Int
0 String
"uv") (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (UExp -> TT Name
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0)))
                                      (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount
-> Maybe ImplicitInfo -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) (Int -> TT Name
forall n. Int -> TT n
V Int
1)))
             Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
ux [(Name, TT Name)]
uf

    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) TT Name
y) (App AppStatus Name
_ TT Name
f TT Name
x)
      | Name -> TT Name -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence Name
n TT Name
y Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
f
        = do [(Name, TT Name)]
ux <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
y TT Name
x
             [(Name, TT Name)]
uf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (Int -> String -> Name
sMN Int
0 String
"uv") (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (UExp -> TT Name
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0)))
                                    (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount
-> Maybe ImplicitInfo -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) (Int -> TT Name
forall n. Int -> TT n
V Int
1))) TT Name
f
             Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
ux [(Name, TT Name)]
uf

    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
x Binder (TT Name)
bx TT Name
sx) (Bind Name
y Binder (TT Name)
by TT Name
sy)
        | Binder (TT Name) -> Binder (TT Name) -> Bool
forall {b} {b}. Binder b -> Binder b -> Bool
sameBinder Binder (TT Name)
bx Binder (TT Name)
by
           = do [(Name, TT Name)]
h1 <- Env
-> [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB Env
env [((Name, Name), TT Name)]
bnames Binder (TT Name)
bx Binder (TT Name)
by
                [(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' ((Name
x, RigCount
RigW, Binder (TT Name)
bx) (Name, RigCount, Binder (TT Name)) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Bool
False (((Name
x,Name
y),Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
bx)((Name, Name), TT Name)
-> [((Name, Name), TT Name)] -> [((Name, Name), TT Name)]
forall a. a -> [a] -> [a]
:[((Name, Name), TT Name)]
bnames) TT Name
sx TT Name
sy
                Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
      where sameBinder :: Binder b -> Binder b -> Bool
sameBinder (Lam RigCount
_ b
_) (Lam RigCount
_ b
_) = Bool
True
            sameBinder (Pi RigCount
_ Maybe ImplicitInfo
i b
_ b
_) (Pi RigCount
_ Maybe ImplicitInfo
i' b
_ b
_) = Bool
True
            sameBinder Binder b
_ Binder b
_ = Bool
False -- never unify holes/guesses/etc
    un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
        | OK Bool
True <- Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
holes TT Name
x TT Name
y = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | TT Name -> Bool
isUniverse TT Name
x Bool -> Bool -> Bool
&& TT Name -> Bool
isUniverse TT Name
y = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                         let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
                                             (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
                         let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
                                     (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                         if (Bool -> Bool
not Bool
r) then TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
err
                           else do UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                                   [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- lift $ tfail err

    unApp :: Env
-> p
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
unApp Env
env p
fn [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App AppStatus Name
_ TT Name
fx TT Name
ax) appy :: TT Name
appy@(App AppStatus Name
_ TT Name
fy TT Name
ay)
        -- shortcut for the common case where we just want to check the
        -- arguments are correct
         | (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name
fx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
fy)
         = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax TT Name
ay
         | (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
fy)
        Bool -> Bool -> Bool
|| (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name -> Bool
metavarApp TT Name
fy Bool -> Bool -> Bool
&& TT Name
ax TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
ay)
        Bool -> Bool -> Bool
|| (TT Name -> Bool
injectiveApp TT Name
fy Bool -> Bool -> Bool
&& TT Name -> Bool
metavarApp TT Name
fx Bool -> Bool -> Bool
&& TT Name
ax TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
ay)
        Bool -> Bool -> Bool
|| (TT Name -> TT Name -> Bool
injectiveTC TT Name
fx TT Name
fy) -- data interface method
         = do let (TT Name
headx, [TT Name]
_) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fx
              let (TT Name
heady, [TT Name]
_) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fy
              -- fail quickly if the heads are disjoint
              TT Name -> TT Name -> StateT UInfo TC [Any]
forall {a} {t :: (* -> *) -> * -> *} {a}.
(Eq a, MonadState UInfo (t TC), MonadTrans t) =>
TT a -> TT a -> t TC [a]
checkHeads TT Name
headx TT Name
heady
              StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall {m :: * -> *} {b}. MonadState UInfo m => m b -> m b -> m b
uplus
                (do [(Name, TT Name)]
hf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
True [((Name, Name), TT Name)]
bnames TT Name
fx TT Name
fy
                    let ax' :: TT Name
ax' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall {a}. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
hf Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ax)
                    let ay' :: TT Name
ay' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall {a}. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
hf Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ay)
                    -- Don't normalise if we don't have to
                    [(Name, TT Name)]
ha <- StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall {m :: * -> *} {b}. MonadState UInfo m => m b -> m b -> m b
uplus (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ax)
                                                      ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ay))
                                (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax' TT Name
ay')
                    Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                    Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
hf [(Name, TT Name)]
ha)
                (do [(Name, TT Name)]
ha <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax TT Name
ay
                    let fx' :: TT Name
fx' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall {a}. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
ha Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fx)
                    let fy' :: TT Name
fy' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall {a}. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
ha Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fy)
                    -- Don't normalise if we don't have to
                    [(Name, TT Name)]
hf <- StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall {m :: * -> *} {b}. MonadState UInfo m => m b -> m b -> m b
uplus (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fx)
                                                      ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fy))
                                (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
fx' TT Name
fy')
                    Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                    Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
hf [(Name, TT Name)]
ha)
       | Bool
otherwise = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
appx TT Name
appy
      where hnormalise :: [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [] Context
_ Env
_ TT Name
t = TT Name
t
            hnormalise [a]
ns Context
ctxt Env
env TT Name
t = Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
t
            checkHeads :: TT a -> TT a -> t TC [a]
checkHeads (P (DCon Int
_ Int
_ Bool
_) a
x TT a
_) (P (DCon Int
_ Int
_ Bool
_) a
y TT a
_)
                | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y = TT Name -> TT Name -> t TC [a]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
            checkHeads (P (TCon Int
_ Int
_) a
x TT a
_) (P (TCon Int
_ Int
_) a
y TT a
_)
                | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y = TT Name -> TT Name -> t TC [a]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
            checkHeads (P (DCon Int
_ Int
_ Bool
_) a
x TT a
_) (P (TCon Int
_ Int
_) a
y TT a
_)
                = TT Name -> TT Name -> t TC [a]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
            checkHeads (P (TCon Int
_ Int
_) a
x TT a
_) (P (DCon Int
_ Int
_ Bool
_) a
y TT a
_)
                = TT Name -> TT Name -> t TC [a]
forall {t :: (* -> *) -> * -> *} {b}.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
            checkHeads TT a
_ TT a
_ = [a] -> t TC [a]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []

            metavarApp :: TT Name -> Bool
metavarApp TT Name
tm = let (TT Name
f, [TT Name]
args) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm in
                                (TT Name -> Bool
metavar TT Name
f Bool -> Bool -> Bool
&&
                                 (TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\TT Name
x -> TT Name -> Bool
metavarApp TT Name
x) [TT Name]
args
                                    Bool -> Bool -> Bool
&& [TT Name] -> [TT Name]
forall a. Eq a => [a] -> [a]
nub [TT Name]
args [TT Name] -> [TT Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [TT Name]
args) Bool -> Bool -> Bool
||
                                       TT Name -> Bool
globmetavar TT Name
tm

            globmetavar :: TT Name -> Bool
globmetavar TT Name
t = case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t  of
                                (P NameType
_ Name
x TT Name
_, [TT Name]
_) ->
                                   case Name -> Context -> [Def]
lookupDef Name
x Context
ctxt of
                                        [TyDecl NameType
_ TT Name
_] -> Bool
True
                                        [Def]
_ -> Bool
False
                                (TT Name, [TT Name])
_ -> Bool
False

            metavar :: TT Name -> Bool
metavar TT Name
t = case TT Name
t of
                             P NameType
_ Name
x TT Name
_ -> (Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
usersupp Bool -> Bool -> Bool
&&
                                             (Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Env -> Name -> Bool
holeIn Env
env Name
x))
                                          Bool -> Bool -> Bool
|| TT Name -> Bool
globmetavar TT Name
t
                             TT Name
_ -> Bool
False

            injectiveTC :: TT Name -> TT Name -> Bool
injectiveTC t :: TT Name
t@(P NameType
Ref Name
n TT Name
_) t' :: TT Name
t'@(P NameType
Ref Name
n' TT Name
_)
                | Just Bool
ni <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt,
                  Just Bool
ni' <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n' Context
ctxt
              = (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& Bool
ni) Bool -> Bool -> Bool
||
                (Bool
ni Bool -> Bool -> Bool
&& TT Name -> Bool
metavar TT Name
t') Bool -> Bool -> Bool
||
                (TT Name -> Bool
metavar TT Name
t Bool -> Bool -> Bool
&& Bool
ni')
            injectiveTC (App AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' TT Name
a') = TT Name -> TT Name -> Bool
injectiveTC TT Name
f TT Name
f'
            injectiveTC TT Name
_ TT Name
_ = Bool
False


    unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
    unifyTmpFail :: TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
x TT Name
y
                  = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                       let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x) (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
                       let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
                                   (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                   (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                       UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
topx, TT Name
topy, Bool
True, Env
env, Err
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    -- shortcut failure, if we *know* nothing can fix it
    unifyFail :: TT Name -> TT Name -> t TC b
unifyFail TT Name
x TT Name
y = do UI Int
s Fails
f <- t TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                       let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x) (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
                       let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
                                   (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                   (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                       UInfo -> t TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
topx, TT Name
topy, Bool
True, Env
env, Err
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       TC b -> t TC b
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err -> TC b
forall a. Err -> TC a
tfail Err
err


    uB :: Env
-> [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB Env
env [((Name, Name), TT Name)]
bnames (Let RigCount
_ TT Name
tx TT Name
vx) (Let RigCount
_ TT Name
ty TT Name
vy)
        = do [(Name, TT Name)]
h1 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
             [(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
             Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
             Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
    uB Env
env [((Name, Name), TT Name)]
bnames (Guess TT Name
tx TT Name
vx) (Guess TT Name
ty TT Name
vy)
        = do [(Name, TT Name)]
h1 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
             [(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
             Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
             Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
    uB Env
env [((Name, Name), TT Name)]
bnames (Lam RigCount
_ TT Name
tx) (Lam RigCount
_ TT Name
ty) = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB Env
env [((Name, Name), TT Name)]
bnames (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
tx TT Name
_) (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
ty TT Name
_) = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1; Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB Env
env [((Name, Name), TT Name)]
bnames (Hole TT Name
tx) (Hole TT Name
ty) = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB Env
env [((Name, Name), TT Name)]
bnames (PVar RigCount
_ TT Name
tx) (PVar RigCount
_ TT Name
ty) = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
    uB Env
env [((Name, Name), TT Name)]
bnames Binder (TT Name)
x Binder (TT Name)
y
                  = do UI Int
s Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                       let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x))
                                           (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y))
                       let err :: Err
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
                                   (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Maybe Provenance
forall a. Maybe a
Nothing) (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s)
                                   (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
                       UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y,
                                   Bool
False,
                                   Env
env, Err
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- lift $ tfail err

    checkCycle :: [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
_ TT Name
_) = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
    checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm (Name
x, TT Name
tm)
        | Context -> Name -> TT Name -> Bool
conGuarded Context
ctxt Name
x TT Name
tm = TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err
forall t. Name -> t -> [(Name, t)] -> Err' t
InfiniteUnify Name
x TT Name
tm (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env))
        | Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TT Name -> [Name]
forall n. Eq n => TT n -> [n]
freeNames TT Name
tm = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
        | Bool
otherwise = [((Name, Name), TT Name)]
-> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall {t :: (* -> *) -> * -> *} {a}.
(MonadTrans t, Monad (t TC)) =>
[((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (Name
x, TT Name
tm)

    checkScope :: [((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) | TT Name -> Bool
pureTerm TT Name
tm =
        let v :: Int
v = Int -> TT Name -> Int
highV (-Int
1) TT Name
tm in
            if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
ns
               then TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"SCOPE ERROR")
               else [(a, TT Name)] -> t TC [(a, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(a
x, Int -> [((Name, Name), TT Name)] -> TT Name -> TT Name
forall {n}. Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
v [((Name, Name), TT Name)]
ns TT Name
tm)]
    checkScope [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) = TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"HOLE ERROR")

    bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
i [((n, n), TT n)]
ns TT n
tm
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = TT n
tm
      | Bool
otherwise = let ((n
x,n
y),TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i in
                        AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
forall n. AppStatus n
MaybeHoles (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
y (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT n
ty) (Int -> [((n, n), TT n)] -> TT n -> TT n
bind (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [((n, n), TT n)]
ns TT n
tm))
                            (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
x TT n
ty)

    combine :: Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
    combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ((Name
n, TT Name
t) : [(Name, TT Name)]
bs)
        = case Name -> [(Name, TT Name)] -> Maybe (TT Name)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, TT Name)]
as of
            Maybe (TT Name)
Nothing -> Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames ([(Name, TT Name)]
as [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name
n,TT Name
t)]) [(Name, TT Name)]
bs
            Just TT Name
t' -> do [(Name, TT Name)]
ns <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
t TT Name
t'
                          -- make sure there's n mapping from n in ns
                          let ns' :: [(Name, TT Name)]
ns' = ((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
x, TT Name
_) -> Name
xName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n) [(Name, TT Name)]
ns
                          Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
1
                          Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ([(Name, TT Name)]
ns' [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)]
bs)

highV :: Int -> Term -> Int
highV :: Int -> TT Name -> Int
highV Int
i (V Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i = Int
j
                | Bool
otherwise = Int
i
highV Int
i (Bind Name
n Binder (TT Name)
b TT Name
sc) = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int
i, Int -> TT Name -> Int
highV Int
i (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b), (Int -> TT Name -> Int
highV Int
i TT Name
sc Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
highV Int
i (App AppStatus Name
_ TT Name
f TT Name
x) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> TT Name -> Int
highV Int
i TT Name
f) (Int -> TT Name -> Int
highV Int
i TT Name
x)
highV Int
i TT Name
_ = Int
i

-- If there are any clashes of constructors, deem it unrecoverable, otherwise some
-- more work may help.
-- FIXME: Depending on how overloading gets used, this may cause problems. Better
-- rethink overloading properly...
-- ASSUMPTION: inputs are in normal form
--
-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
--
recoverable :: TT Name -> TT Name -> Bool
recoverable t :: TT Name
t@(App AppStatus Name
_ TT Name
_ TT Name
_) TT Name
_
    | (P NameType
_ (UN Text
l) TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t, Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delayed" = Bool
False
recoverable TT Name
_ t :: TT Name
t@(App AppStatus Name
_ TT Name
_ TT Name
_)
    | (P NameType
_ (UN Text
l) TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t, Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delayed" = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (TType UExp
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (UType Universe
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
x) (Constant Const
y) = Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (TType UExp
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (UType Universe
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (Constant Const
_) = Bool
False
recoverable (TType UExp
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (UType Universe
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (TType UExp
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (UType Universe
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (Constant Const
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable p :: TT Name
p@(TType UExp
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(UType Universe
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(Constant Const
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(TType UExp
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(UType Universe
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(Constant Const
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable p :: TT Name
p@(P NameType
_ Name
n TT Name
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(P NameType
_ Name
_ TT Name
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' TT Name
a')
    | TT Name
f TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
f' = TT Name -> TT Name -> Bool
recoverable TT Name
a TT Name
a'
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' TT Name
a')
    = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
f' -- && recoverable a a'
recoverable TT Name
f (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc)
    | (P (DCon Int
_ Int
_ Bool
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (P (TCon Int
_ Int
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (Constant Const
_) <- TT Name
f = Bool
False
    | TType UExp
_ <- TT Name
f = Bool
False
    | UType Universe
_ <- TT Name
f = Bool
False
recoverable (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc) TT Name
f
    | (P (DCon Int
_ Int
_ Bool
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (P (TCon Int
_ Int
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (Constant Const
_) <- TT Name
f = Bool
False
    | TType UExp
_ <- TT Name
f = Bool
False
    | UType Universe
_ <- TT Name
f = Bool
False
recoverable (Bind Name
_ (Lam RigCount
_ TT Name
_) TT Name
sc) TT Name
f = TT Name -> TT Name -> Bool
recoverable TT Name
sc TT Name
f
recoverable TT Name
f (Bind Name
_ (Lam RigCount
_ TT Name
_) TT Name
sc) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
sc
recoverable TT Name
x TT Name
y = Bool
True

errEnv :: [(a, r, Binder b)] -> [(a, b)]
errEnv :: forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv = ((a, r, Binder b) -> (a, b)) -> [(a, r, Binder b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
x, r
_, Binder b
b) -> (a
x, Binder b -> b
forall b. Binder b -> b
binderTy Binder b
b))

holeIn :: Env -> Name -> Bool
holeIn :: Env -> Name -> Bool
holeIn Env
env Name
n = case Name -> Env -> Maybe (Binder (TT Name))
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
                    Just (Hole TT Name
_) -> Bool
True
                    Just (Guess TT Name
_ TT Name
_) -> Bool
True
                    Maybe (Binder (TT Name))
_ -> Bool
False