{-|
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
showList :: [FailAt] -> ShowS
$cshowList :: [FailAt] -> ShowS
show :: FailAt -> String
$cshow :: FailAt -> String
showsPrec :: Int -> FailAt -> ShowS
$cshowsPrec :: Int -> FailAt -> ShowS
Show, FailAt -> FailAt -> Bool
(FailAt -> FailAt -> Bool)
-> (FailAt -> FailAt -> Bool) -> Eq FailAt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FailAt -> FailAt -> Bool
$c/= :: FailAt -> FailAt -> Bool
== :: FailAt -> FailAt -> Bool
$c== :: 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
/= :: FailContext -> FailContext -> Bool
$c/= :: FailContext -> FailContext -> Bool
== :: FailContext -> FailContext -> Bool
$c== :: 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
showList :: [FailContext] -> ShowS
$cshowList :: [FailContext] -> ShowS
show :: FailContext -> String
$cshow :: FailContext -> String
showsPrec :: Int -> FailContext -> ShowS
$cshowsPrec :: Int -> 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' (TT Name), [FailContext],
  FailAt)
 -> Bool)
-> Fails -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TT Name, TT Name, Bool, Env, Err' (TT Name), [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 (_,_,_,_, err :: Err' t
err, _, _) = Err' t -> Bool
forall t. Err' t -> Bool
unrec Err' t
err

        unrec :: Err' t -> Bool
unrec (CantUnify r :: Bool
r _ _ _ _ _) = Bool -> Bool
not Bool
r
        unrec (At _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec (Elaborating _ _ _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec (ElaboratingArg _ _ _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
        unrec _ = 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
showList :: [UInfo] -> ShowS
$cshowList :: [UInfo] -> ShowS
show :: UInfo -> String
$cshow :: UInfo -> String
showsPrec :: Int -> UInfo -> ShowS
$cshowsPrec :: Int -> 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 :: [FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [] r :: Bool
r t1 :: (t, Maybe Provenance)
t1 t2 :: (t, Maybe Provenance)
t2 e :: Err' t
e ctxt :: [(Name, t)]
ctxt i :: 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
fc f :: Name
f x :: Name
x : prev :: [FailContext]
prev) r :: Bool
r t1 :: (t, Maybe Provenance)
t1 t2 :: (t, Maybe Provenance)
t2 e :: Err' t
e ctxt :: [(Name, t)]
ctxt i :: 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 _ f' :: Name
f' x' :: 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 ctxt :: Context
ctxt env :: Env
env (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) inj :: [Name]
inj holes :: [Name]
holes from :: [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 0 []) of
        OK (v :: [(Name, TT Name)]
v, UI _ []) ->
           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 (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')
        res :: 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 0 []) of
                       OK (v :: [(Name, TT Name)]
v, UI _ fails :: 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 (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 e :: Err' (TT Name)
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 0 []) of
                           OK (v :: [(Name, TT Name)]
v, UI _ fails :: 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 (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')
                           _ -> Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
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 names :: [((Name, Name), TT Name)]
names tx :: TT Name
tx@(P _ x :: Name
x _) tm :: 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 (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 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 names :: [((Name, Name), TT Name)]
names tm :: TT Name
tm ty :: TT Name
ty@(P _ y :: Name
y _)
        | 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 (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 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 bnames :: [((Name, Name), TT Name)]
bnames (V i :: Int
i) (P _ x :: Name
x _)
        | [((Name, Name), TT Name)] -> 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. [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. [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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un bnames :: [((Name, Name), TT Name)]
bnames (P _ x :: Name
x _) (V i :: Int
i)
        | [((Name, Name), TT Name)] -> 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. [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. [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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un bnames :: [((Name, Name), TT Name)]
bnames (Bind x :: Name
x bx :: Binder (TT Name)
bx sx :: TT Name
sx) (Bind y :: Name
y by :: Binder (TT Name)
by sy :: 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 names :: [((Name, Name), TT Name)]
names (App _ fx :: TT Name
fx ax :: TT Name
ax) (App _ fy :: TT Name
fy ay :: 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 names :: [((Name, Name), TT Name)]
names x :: TT Name
x y :: TT Name
y
        | OK 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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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 (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' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
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' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                                   TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err


    uB :: [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB bnames :: [((Name, Name), TT Name)]
bnames (Let _ tx :: TT Name
tx vx :: TT Name
vx) (Let _ ty :: TT Name
ty vy :: 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 bnames :: [((Name, Name), TT Name)]
bnames (Lam _ tx :: TT Name
tx) (Lam _ ty :: 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 bnames :: [((Name, Name), TT Name)]
bnames (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i tx :: TT Name
tx _) (Pi r' :: RigCount
r' i' :: Maybe ImplicitInfo
i' ty :: 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 bnames :: [((Name, Name), TT Name)]
bnames x :: Binder (TT Name)
x y :: Binder (TT Name)
y = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

    notHole :: Binder b -> Bool
notHole (Hole _) = Bool
False
    notHole _ = 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 i :: Int
i = do UI s :: Int
s f :: 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 x :: TT Name
x y :: TT Name
y = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       TC b -> t TC b
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' (TT Name) -> TC b
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
    combine :: [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
    combine bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as ((n :: Name
n, t :: TT Name
t) : bs :: [(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
            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 t' :: 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 (\ (x :: Name
x, _) -> 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 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 ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ x' :: Name
x' _) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ _ _) = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
    checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm (x :: Name
x, tm :: 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 (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' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err' (TT Name)
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 (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 ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) =
        let v :: Int
v = Int -> TT Name -> Int
highV (-1) TT Name
tm in
            if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> 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 (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' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "SCOPE ERROR")
               else [(a, TT Name)] -> t TC [(a, TT Name)]
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 i :: Int
i ns :: [((n, n), TT n)]
ns tm :: TT n
tm
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = TT n
tm
      | Bool
otherwise = let ((x :: n
x,y :: n
y),ty :: TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. [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
-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
env (x :: a
x, t :: 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
env tm :: 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 env :: [Name]
env (Bind n :: Name
n b :: Binder (TT Name)
b sc :: TT Name
sc)
        | Name
n Name -> [Name] -> 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 (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 n. Eq n => n -> n -> TT n -> TT n
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 (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 env :: [Name]
env (App s :: AppStatus Name
s f :: TT Name
f a :: 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 env :: [Name]
env t :: TT Name
t = TT Name
t

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

    explicitHole :: TT n -> TT n
explicitHole (Bind n :: n
n (Hole ty :: TT n
ty) sc :: 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 t :: 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 (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) from :: [FailContext]
from env :: [(Name, r, Binder (TT Name))]
env topns :: [(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@(x :: a
x, P _ x' :: a
x' _) : ns :: [(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 (\t :: (a, TT a)
t -> case (a, TT a)
t of
                                      (n :: a
n, P _ n' :: a
n' _) -> 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)
                                      _ -> Bool
True) [(a, TT a)]
ns)
        dropPairs (n :: (a, TT a)
n : ns :: [(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 vs :: [(a, a)]
vs [] = [(a, TT a)] -> TC [(a, TT a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        followSols vs :: [(a, a)]
vs ((n :: a
n, P _ t :: a
t _) : ns :: [(a, TT a)]
ns)
          | Just t' :: 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 _ tn :: a
tn _ ->
                           if (a
n, a
tn) (a, a) -> [(a, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
vs then -- cycle
                                   Err' (TT Name) -> TC [(a, a)]
forall a. Err' (TT Name) -> TC a
tfail ([FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") ([(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) 0)
                                   else [(a, a)] -> TC [(a, 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)
                     _ -> [(a, a)] -> TC [(a, 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 vs :: [(a, a)]
vs (n :: (a, TT a)
n : ns :: [(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 (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 ctxt :: Context
ctxt env :: Env
env (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) inj :: [Name]
inj holes :: [Name]
holes usersupp :: [Name]
usersupp from :: [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 0 []) of
        OK (v :: [(Name, TT Name)]
v, UI _ []) -> 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 (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', [])
        res :: 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 0 []) of
                       OK (v :: [(Name, TT Name)]
v, UI _ fails :: 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 (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 e :: Err' (TT Name)
e -> Err' (TT Name) -> TC ([(Name, TT Name)], Fails)
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
e
  where
    injective :: TT n -> Bool
injective (P (DCon _ _ _) _ _) = Bool
True
    injective (P (TCon _ _) _ _) = Bool
True
--     injective (P Ref n _)
--          | Just i <- lookupInjectiveExact n ctxt = i
    injective (App _ f :: TT n
f a :: TT n
a)        = TT n -> Bool
injective TT n
f -- && injective a
    injective _                  = 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 _ n :: Name
n _)        = Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj
    injectiveVar (App _ f :: TT Name
f a :: TT Name
a)      = TT Name -> Bool
injectiveVar TT Name
f -- && injective a
    injectiveVar _ = Bool
False

    injectiveApp :: TT Name -> Bool
injectiveApp x :: 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 _ _ _) = Bool
False
    notP _ = Bool
True

    sc :: Int -> m ()
sc i :: Int
i = do UI s :: Int
s f :: 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 u1 :: m b
u1 u2 :: m b
u2 = do UI s :: Int
s f :: Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                     b
r <- m b
u1
                     UI s :: Int
s f' :: Fails
f' <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
                     if (Fails -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f')
                        then b -> m b
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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names x :: TT Name
x y :: 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 (m :: * -> *) a. Monad m => a -> m a
return [] -- shortcut
    un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon _ _ _) x :: Name
x _) topy :: TT Name
topy@(P (DCon _ _ _) y :: Name
y _)
                | 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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(P (TCon _ _) y :: Name
y _)
                | 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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon _ _ _) x :: Name
x _) topy :: TT Name
topy@(P (TCon _ _) y :: 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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(P (DCon _ _ _) y :: 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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Constant _) topy :: TT Name
topy@(P (TCon _ _) y :: 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
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(Constant _)
                = 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tx :: TT Name
tx@(P _ x :: Name
x _) ty :: TT Name
ty@(P _ y :: Name
y _)
        | (Name
x,Name
y) (Name, Name) -> [(Name, Name)] -> 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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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 (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 (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 (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 (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 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 0 Name
y Env
env) of
                   LT -> do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 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)
                   _ -> do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 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 i :: t
i n :: t
n ((n' :: t
n',_,_):env :: [(t, b, c)]
env) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
n' = t
i
             envPos i :: t
i n :: t
n (_:env :: [(t, b, c)]
env) = t -> t -> [(t, b, c)] -> t
envPos (t
it -> t -> t
forall a. Num a => a -> a -> a
+1) t
n [(t, b, c)]
env
             envPos _ _ _ = 100000
    un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames xtm :: TT Name
xtm@(P _ x :: Name
x _) tm :: 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
                       = do UI s :: Int
s f :: 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 1
                                         [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tm :: TT Name
tm ytm :: TT Name
ytm@(P _ y :: Name
y _)
        | TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
                       = do UI s :: Int
s f :: 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 1
                                         [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (V i :: Int
i) (P _ x :: Name
x _)
        | [((Name, Name), TT Name)] -> 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. [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. [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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (P _ x :: Name
x _) (V i :: Int
i)
        | [((Name, Name), TT Name)] -> 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. [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. [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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

    un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Bind n :: Name
n (Hole t :: TT Name
t) sc :: TT Name
sc) y :: TT Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
topx TT Name
y
    un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names x :: TT Name
x topy :: TT Name
topy@(Bind n :: Name
n (Hole t :: TT Name
t) sc :: 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tm :: TT Name
tm app :: TT Name
app@(App _ _ _)
        | (mvtm :: TT Name
mvtm@(P _ mv :: Name
mv _), args :: [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 (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 n. Eq n => [(n, RigCount, TT n)] -> TT n -> TT n
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 i :: Int
i) = Bool
True
            rigid (P _ t :: Name
t _) = Name
t Name -> [Name] -> 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
            rigid _ = Bool
False

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

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

            containsOnly :: t Name -> [Int] -> TT Name -> Bool
containsOnly args :: t Name
args vs :: [Int]
vs (V i :: Int
i) = Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
vs
            containsOnly args :: t Name
args vs :: [Int]
vs (P Bound n :: Name
n ty :: TT Name
ty)
                   = Name
n Name -> t Name -> 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 args :: t Name
args vs :: [Int]
vs (P _ n :: Name
n ty :: TT Name
ty)
                   = Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
n Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> 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 args :: t Name
args vs :: [Int]
vs (App _ f :: TT Name
f a :: 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 args :: t Name
args vs :: [Int]
vs (Bind _ b :: Binder (TT Name)
b sc :: 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 (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
+1) [Int]
vs) TT Name
sc
            containsOnly args :: t Name
args vs :: [Int]
vs _ = Bool
True

            bindLams :: [TT Name] -> TT Name -> TT Name
bindLams [] tm :: TT Name
tm = TT Name
tm
            bindLams (a :: TT Name
a : as :: [TT Name]
as) tm :: 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 i :: Int
i) tm :: 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. [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. [a] -> Int -> a
!! Int
i))))
                                    TT Name
tm
            bindLam (P _ n :: Name
n ty :: TT Name
ty) tm :: 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 _ tm :: TT Name
tm = String -> TT Name
forall a. HasCallStack => String -> a
error "Can't happen [non rigid bindLam]"

            substEnv :: [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [] tm :: TT n
tm = TT n
tm
            substEnv ((n :: n
n, _, t :: Binder (TT n)
t) : env :: [(n, b, Binder (TT n))]
env) tm :: 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 :: [(n, RigCount, TT n)] -> TT n -> TT n
eta ks :: [(n, RigCount, TT n)]
ks (Bind n :: n
n (Lam r :: RigCount
r ty :: TT n
ty) sc :: TT n
sc) = [(n, RigCount, TT n)] -> TT n -> TT n
eta ((n
n, RigCount
r, TT n
ty) (n, RigCount, TT n)
-> [(n, RigCount, TT n)] -> [(n, RigCount, TT n)]
forall a. a -> [a] -> [a]
: [(n, RigCount, TT n)]
ks) TT n
sc
            eta ks :: [(n, RigCount, TT n)]
ks t :: TT n
t = [(n, RigCount, TT n)] -> TT n -> TT n
rebind [(n, RigCount, TT n)]
ks TT n
t

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

    un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App _ _ _) appy :: TT Name
appy@(App _ _ _)
        = 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (P Bound n' :: Name
n' _)))
        | 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (P Bound n' :: Name
n' _))) y :: 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (V 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (V 0))) y :: 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (App _ f :: TT Name
f x :: TT Name
x) (Bind n :: Name
n (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i t :: TT Name
t k :: TT Name
k) y :: 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 0 "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 [] 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 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i t :: TT Name
t k :: TT Name
k) y :: TT Name
y) (App _ f :: TT Name
f x :: 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 0 "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 [] 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 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
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind x :: Name
x bx :: Binder (TT Name)
bx sx :: TT Name
sx) (Bind y :: Name
y by :: Binder (TT Name)
by sy :: 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 _ _) (Lam _ _) = Bool
True
            sameBinder (Pi _ i :: Maybe ImplicitInfo
i _ _) (Pi _ i' :: Maybe ImplicitInfo
i' _ _) = Bool
True
            sameBinder _ _ = Bool
False -- never unify holes/guesses/etc
    un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x y :: TT Name
y
        | OK 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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        | Bool
otherwise = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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 (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' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
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' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                                   [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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
env fn :: p
fn bnames :: [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App _ fx :: TT Name
fx ax :: TT Name
ax) appy :: TT Name
appy@(App _ fy :: TT Name
fy ay :: 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 (headx :: TT Name
headx, _) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fx
              let (heady :: TT Name
heady, _) = 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 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 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 [] _ _ t :: TT Name
t = TT Name
t
            hnormalise ns :: [a]
ns ctxt :: Context
ctxt env :: Env
env t :: 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 _ _ _) x :: a
x _) (P (DCon _ _ _) y :: a
y _)
                | 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 _ _) x :: a
x _) (P (TCon _ _) y :: a
y _)
                | 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 _ _ _) x :: a
x _) (P (TCon _ _) y :: 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 _ _) x :: a
x _) (P (DCon _ _ _) y :: 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 _ _ = [a] -> t TC [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

            metavarApp :: TT Name -> Bool
metavarApp tm :: TT Name
tm = let (f :: TT Name
f, args :: [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 (\x :: 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 t :: TT Name
t = case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t  of
                                (P _ x :: Name
x _, _) ->
                                   case Name -> Context -> [Def]
lookupDef Name
x Context
ctxt of
                                        [TyDecl _ _] -> Bool
True
                                        _ -> Bool
False
                                _ -> Bool
False

            metavar :: TT Name -> Bool
metavar t :: TT Name
t = case TT Name
t of
                             P _ x :: Name
x _ -> (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 (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
                             _ -> Bool
False

            injectiveTC :: TT Name -> TT Name -> Bool
injectiveTC t :: TT Name
t@(P Ref n :: Name
n _) t' :: TT Name
t'@(P Ref n' :: Name
n' _)
                | Just ni :: Bool
ni <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt,
                  Just ni' :: 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 _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: TT Name
a') = TT Name -> TT Name -> Bool
injectiveTC TT Name
f TT Name
f'
            injectiveTC _ _ = Bool
False


    unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
    unifyTmpFail :: TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail x :: TT Name
x y :: TT Name
y
                  = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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 x :: TT Name
x y :: TT Name
y = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       TC b -> t TC b
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' (TT Name) -> TC b
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err


    uB :: Env
-> [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Let _ tx :: TT Name
tx vx :: TT Name
vx) (Let _ ty :: TT Name
ty vy :: 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 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
env bnames :: [((Name, Name), TT Name)]
bnames (Guess tx :: TT Name
tx vx :: TT Name
vx) (Guess ty :: TT Name
ty vy :: 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 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
env bnames :: [((Name, Name), TT Name)]
bnames (Lam _ tx :: TT Name
tx) (Lam _ ty :: TT Name
ty) = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 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
env bnames :: [((Name, Name), TT Name)]
bnames (Pi _ _ tx :: TT Name
tx _) (Pi _ _ ty :: TT Name
ty _) = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 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
env bnames :: [((Name, Name), TT Name)]
bnames (Hole tx :: TT Name
tx) (Hole ty :: 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
env bnames :: [((Name, Name), TT Name)]
bnames (PVar _ tx :: TT Name
tx) (PVar _ ty :: 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
env bnames :: [((Name, Name), TT Name)]
bnames x :: Binder (TT Name)
x y :: Binder (TT Name)
y
                  = do UI s :: Int
s f :: 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' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
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' (TT Name)
forall t. String -> Err' t
Msg "") (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' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
 FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
                       [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
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 ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ _ _) = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
    checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm (x :: Name
x, tm :: 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 (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' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err' (TT Name)
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 (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 ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) | TT Name -> Bool
pureTerm TT Name
tm =
        let v :: Int
v = Int -> TT Name -> Int
highV (-1) TT Name
tm in
            if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> 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 (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' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "SCOPE ERROR")
               else [(a, TT Name)] -> t TC [(a, TT Name)]
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 ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) = TC [(a, TT Name)] -> t TC [(a, TT Name)]
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' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "HOLE ERROR")

    bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind i :: Int
i ns :: [((n, n), TT n)]
ns tm :: TT n
tm
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = TT n
tm
      | Bool
otherwise = let ((x :: n
x,y :: n
y),ty :: TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. [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
-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
env bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
    combine env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as ((n :: Name
n, t :: TT Name
t) : bs :: [(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
            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 t' :: 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 (\ (x :: Name
x, _) -> 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 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 i :: Int
i (V j :: Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i = Int
j
                | Bool
otherwise = Int
i
highV i :: Int
i (Bind n :: Name
n b :: Binder (TT Name)
b sc :: TT Name
sc) = [Int] -> Int
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
- 1)]
highV i :: Int
i (App _ f :: TT Name
f x :: 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 i :: Int
i _ = 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 _ _ _) _
    | (P _ (UN l :: Text
l) _, _) <- 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 "Delayed" = Bool
False
recoverable _ t :: TT Name
t@(App _ _ _)
    | (P _ (UN l :: Text
l) _, _) <- 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 "Delayed" = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (P (DCon _ _ _) y :: Name
y _) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (P (TCon _ _) x :: Name
x _) (P (TCon _ _) y :: Name
y _) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (TType _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (UType _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (Constant _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (Constant x :: Const
x) (Constant y :: Const
y) = Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y
recoverable (P (DCon _ _ _) x :: Name
x _) (TType _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (UType _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (Constant _) = Bool
False
recoverable (TType _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (UType _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (Constant _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (TType _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (UType _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (Constant _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable p :: TT Name
p@(TType _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(UType _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(Constant _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(TType _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(UType _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(Constant _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable p :: TT Name
p@(P _ n :: Name
n _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(P _ _ _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: 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 _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: TT Name
a')
    = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
f' -- && recoverable a a'
recoverable f :: TT Name
f (Bind _ (Pi _ _ _ _) sc :: TT Name
sc)
    | (P (DCon _ _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (P (TCon _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (Constant _) <- TT Name
f = Bool
False
    | TType _ <- TT Name
f = Bool
False
    | UType _ <- TT Name
f = Bool
False
recoverable (Bind _ (Pi _ _ _ _) sc :: TT Name
sc) f :: TT Name
f
    | (P (DCon _ _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (P (TCon _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
    | (Constant _) <- TT Name
f = Bool
False
    | TType _ <- TT Name
f = Bool
False
    | UType _ <- TT Name
f = Bool
False
recoverable (Bind _ (Lam _ _) sc :: TT Name
sc) f :: TT Name
f = TT Name -> TT Name -> Bool
recoverable TT Name
sc TT Name
f
recoverable f :: TT Name
f (Bind _ (Lam _ _) sc :: TT Name
sc) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
sc
recoverable x :: TT Name
x y :: TT Name
y = Bool
True

errEnv :: [(a, r, Binder b)] -> [(a, b)]
errEnv :: [(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 (\(x :: a
x, _, b :: 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
env n :: 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 _) -> Bool
True
                    Just (Guess _ _) -> Bool
True
                    _ -> Bool
False