module MatchSigs.Matching
  ( MatchedSigs(..)
  ) where

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

import           Name

import           MatchSigs.Matching.Env
import           MatchSigs.Sig

type SigMatches = ( [Sig FreeVarIdx] -- Sig shared by these 'Name's
                  , String -- rendered sig
                  , [Name] -- Names that share this signature
                  )

newtype MatchedSigs =
  MatchedSigs { MatchedSigs -> [SigMatches]
getMatchedSigs :: [SigMatches] }

instance Semigroup MatchedSigs where
  <> :: MatchedSigs -> MatchedSigs -> MatchedSigs
(<>) = MatchedSigs -> MatchedSigs -> MatchedSigs
unionMatchedSigs

instance Monoid MatchedSigs where
  mempty :: MatchedSigs
mempty = [SigMatches] -> MatchedSigs
MatchedSigs [SigMatches]
forall a. Monoid a => a
mempty

-- | Create the union of two 'MatchedSigs' by checking if there a match in one
-- group for each sig in the other.
-- This is O(n^2) since there is no suitable ordering for sigs due to different
-- potential ordering of free vars.
unionMatchedSigs :: MatchedSigs -> MatchedSigs -> MatchedSigs
unionMatchedSigs :: MatchedSigs -> MatchedSigs -> MatchedSigs
unionMatchedSigs (MatchedSigs [SigMatches]
a) (MatchedSigs [SigMatches]
b)
  = [SigMatches] -> MatchedSigs
MatchedSigs
  ([SigMatches] -> MatchedSigs)
-> (([SigMatches], [SigMatches]) -> [SigMatches])
-> ([SigMatches], [SigMatches])
-> MatchedSigs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SigMatches] -> [SigMatches] -> [SigMatches])
-> ([SigMatches], [SigMatches]) -> [SigMatches]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [SigMatches] -> [SigMatches] -> [SigMatches]
forall a. [a] -> [a] -> [a]
(++)
  -- fold compatible sigs from b in a, append the ones that are not compatible
  (([SigMatches], [SigMatches]) -> MatchedSigs)
-> ([SigMatches], [SigMatches]) -> MatchedSigs
forall a b. (a -> b) -> a -> b
$ (([SigMatches], [SigMatches])
 -> SigMatches -> ([SigMatches], [SigMatches]))
-> ([SigMatches], [SigMatches])
-> [SigMatches]
-> ([SigMatches], [SigMatches])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([SigMatches], [SigMatches])
-> SigMatches -> ([SigMatches], [SigMatches])
forall (t :: * -> *).
Foldable t =>
(t SigMatches, [SigMatches])
-> SigMatches -> ([SigMatches], [SigMatches])
go ([SigMatches]
a, []) [SigMatches]
b
  where
    go :: (t SigMatches, [SigMatches])
-> SigMatches -> ([SigMatches], [SigMatches])
go (t SigMatches
aSigs, [SigMatches]
nonMatches) SigMatches
bSig
      = let check :: ([SigMatches], Bool) -> SigMatches -> ([SigMatches], Bool)
check ([SigMatches]
ss, Bool
False) SigMatches
aSig
              = case SigMatches -> SigMatches -> Maybe SigMatches
compatibleSigs SigMatches
aSig SigMatches
bSig of
                  Just SigMatches
s' -> (SigMatches
s' SigMatches -> [SigMatches] -> [SigMatches]
forall a. a -> [a] -> [a]
: [SigMatches]
ss, Bool
True)
                  Maybe SigMatches
Nothing -> (SigMatches
aSig SigMatches -> [SigMatches] -> [SigMatches]
forall a. a -> [a] -> [a]
: [SigMatches]
ss, Bool
False)
            check ([SigMatches]
ss, Bool
True) SigMatches
aSig = (SigMatches
aSig SigMatches -> [SigMatches] -> [SigMatches]
forall a. a -> [a] -> [a]
: [SigMatches]
ss, Bool
True)
         in case (([SigMatches], Bool) -> SigMatches -> ([SigMatches], Bool))
-> ([SigMatches], Bool) -> t SigMatches -> ([SigMatches], Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([SigMatches], Bool) -> SigMatches -> ([SigMatches], Bool)
check ([], Bool
False) t SigMatches
aSigs of
              ([SigMatches]
res, Bool
False) -> ([SigMatches]
res, SigMatches
bSig SigMatches -> [SigMatches] -> [SigMatches]
forall a. a -> [a] -> [a]
: [SigMatches]
nonMatches)
              ([SigMatches]
res, Bool
True) -> ([SigMatches]
res, [SigMatches]
nonMatches)

-- | Combines the names in two 'SigMatches' if the sigs match
compatibleSigs :: SigMatches -> SigMatches -> Maybe SigMatches
compatibleSigs :: SigMatches -> SigMatches -> Maybe SigMatches
compatibleSigs ([Sig FreeVarIdx]
sigA, String
str, [Name]
namesA) ([Sig FreeVarIdx]
sigB, String
_, [Name]
namesB) =
  if State Env Bool -> Env -> Bool
forall s a. State s a -> s -> a
evalState ([Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
sigA [Sig FreeVarIdx]
sigB) Env
initEnv
     then SigMatches -> Maybe SigMatches
forall a. a -> Maybe a
Just ([Sig FreeVarIdx]
sigA, String
str, [Name]
namesA [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
namesB)
     else Maybe SigMatches
forall a. Maybe a
Nothing

-- | Check that two sigs are isomorphic
-- First step is to check that the contexts match.
checkMatch :: [Sig FreeVarIdx]
           -> [Sig FreeVarIdx]
           -> State Env Bool
-- VarCtx and Qual are both expected to occur at the front of the list
checkMatch :: [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch (VarCtx [FreeVarIdx]
va : [Sig FreeVarIdx]
restA) (VarCtx [FreeVarIdx]
vb : [Sig FreeVarIdx]
restB)
  = [FreeVarIdx] -> [FreeVarIdx] -> State Env Bool
introVars [FreeVarIdx]
va [FreeVarIdx]
vb
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
checkMatch (VarCtx [FreeVarIdx]
_ : [Sig FreeVarIdx]
_) [Sig FreeVarIdx]
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
checkMatch [Sig FreeVarIdx]
_ (VarCtx [FreeVarIdx]
_ : [Sig FreeVarIdx]
_) = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- Appearance order of quals not significant
checkMatch (Qual [Sig FreeVarIdx]
qa : [Sig FreeVarIdx]
restA) bs :: [Sig FreeVarIdx]
bs@(Qual [Sig FreeVarIdx]
_ : [Sig FreeVarIdx]
_) =
  let ([Sig FreeVarIdx]
qualsB, [Sig FreeVarIdx]
restB) = (Sig FreeVarIdx -> Bool)
-> [Sig FreeVarIdx] -> ([Sig FreeVarIdx], [Sig FreeVarIdx])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Sig FreeVarIdx -> Bool
forall a. Sig a -> Bool
isQual [Sig FreeVarIdx]
bs
      splits :: [([Sig FreeVarIdx], [Sig FreeVarIdx])]
splits = [[Sig FreeVarIdx]]
-> [[Sig FreeVarIdx]] -> [([Sig FreeVarIdx], [Sig FreeVarIdx])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Sig FreeVarIdx] -> [[Sig FreeVarIdx]]
forall a. [a] -> [[a]]
inits [Sig FreeVarIdx]
qualsB) ([Sig FreeVarIdx] -> [[Sig FreeVarIdx]]
forall a. [a] -> [[a]]
tails [Sig FreeVarIdx]
qualsB)
      go :: ([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool
go ([Sig FreeVarIdx]
i, Qual [Sig FreeVarIdx]
f : [Sig FreeVarIdx]
rest)
        = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
qa [Sig FreeVarIdx]
f
       State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
restA ([Sig FreeVarIdx]
i [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> [Sig FreeVarIdx]
forall a. [a] -> [a] -> [a]
++ [Sig FreeVarIdx]
rest [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> [Sig FreeVarIdx]
forall a. [a] -> [a] -> [a]
++ [Sig FreeVarIdx]
restB)
      go ([Sig FreeVarIdx], [Sig FreeVarIdx])
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
   in [State Env Bool] -> State Env Bool
forall env. [State env Bool] -> State env Bool
checkOr ([State Env Bool] -> State Env Bool)
-> [State Env Bool] -> State Env Bool
forall a b. (a -> b) -> a -> b
$ ([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool
go (([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool)
-> [([Sig FreeVarIdx], [Sig FreeVarIdx])] -> [State Env Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Sig FreeVarIdx], [Sig FreeVarIdx])]
splits
checkMatch (Qual [Sig FreeVarIdx]
_ : [Sig FreeVarIdx]
_) [Sig FreeVarIdx]
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
checkMatch [Sig FreeVarIdx]
_ (Qual [Sig FreeVarIdx]
_ : [Sig FreeVarIdx]
_) = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

checkMatch [Sig FreeVarIdx]
sa [Sig FreeVarIdx]
sb = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkResult [Sig FreeVarIdx]
sa [Sig FreeVarIdx]
sb

-- | Extract the result types and make sure they match before going any further.
checkResult :: [Sig FreeVarIdx]
            -> [Sig FreeVarIdx]
            -> State Env Bool
checkResult :: [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkResult [Sig FreeVarIdx]
sa [Sig FreeVarIdx]
sb
  | Sig FreeVarIdx
ra : [Sig FreeVarIdx]
restA <- [Sig FreeVarIdx] -> [Sig FreeVarIdx]
forall a. [a] -> [a]
reverse [Sig FreeVarIdx]
sa
  , Sig FreeVarIdx
rb : [Sig FreeVarIdx]
restB <- [Sig FreeVarIdx] -> [Sig FreeVarIdx]
forall a. [a] -> [a]
reverse [Sig FreeVarIdx]
sb
  = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx
ra] [Sig FreeVarIdx
rb]
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
checkResult [Sig FreeVarIdx]
_ [Sig FreeVarIdx]
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

-- | After the result type has been removed, check the argument types.
checkArguments :: [Sig FreeVarIdx]
               -> [Sig FreeVarIdx]
               -> State Env Bool
checkArguments :: [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [] [] = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
checkArguments (FreeVar FreeVarIdx
ai : [Sig FreeVarIdx]
restA) (FreeVar FreeVarIdx
bi : [Sig FreeVarIdx]
restB)
  = FreeVarIdx -> FreeVarIdx -> State Env Bool
tryAssignVar FreeVarIdx
ai FreeVarIdx
bi
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB

checkArguments (TyDescriptor FastString
sa Maybe Name
na : [Sig FreeVarIdx]
restA) (TyDescriptor FastString
sb Maybe Name
nb : [Sig FreeVarIdx]
restB)
  | FastString
sa FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
sb
  , Maybe Name
na Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Name
nb
  = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
  | Bool
otherwise = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- this is where we need to check for a failure and rotate the list
checkArguments (Arg [Sig FreeVarIdx]
aa : [Sig FreeVarIdx]
restA) [Sig FreeVarIdx]
sb =
  let splits :: [([Sig FreeVarIdx], [Sig FreeVarIdx])]
splits = [[Sig FreeVarIdx]]
-> [[Sig FreeVarIdx]] -> [([Sig FreeVarIdx], [Sig FreeVarIdx])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Sig FreeVarIdx] -> [[Sig FreeVarIdx]]
forall a. [a] -> [[a]]
inits [Sig FreeVarIdx]
sb) ([Sig FreeVarIdx] -> [[Sig FreeVarIdx]]
forall a. [a] -> [[a]]
tails [Sig FreeVarIdx]
sb)
      go :: ([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool
go ([Sig FreeVarIdx]
i, Arg [Sig FreeVarIdx]
ab : [Sig FreeVarIdx]
rest)
        = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
aa [Sig FreeVarIdx]
ab
       State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA ([Sig FreeVarIdx]
i [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> [Sig FreeVarIdx]
forall a. [a] -> [a] -> [a]
++ [Sig FreeVarIdx]
rest)
      go ([Sig FreeVarIdx], [Sig FreeVarIdx])
_  = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
   in [State Env Bool] -> State Env Bool
forall env. [State env Bool] -> State env Bool
checkOr ([State Env Bool] -> State Env Bool)
-> [State Env Bool] -> State Env Bool
forall a b. (a -> b) -> a -> b
$ ([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool
go (([Sig FreeVarIdx], [Sig FreeVarIdx]) -> State Env Bool)
-> [([Sig FreeVarIdx], [Sig FreeVarIdx])] -> [State Env Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Sig FreeVarIdx], [Sig FreeVarIdx])]
splits

checkArguments (Apply [Sig FreeVarIdx]
ca [[Sig FreeVarIdx]]
aa : [Sig FreeVarIdx]
restA) (Apply [Sig FreeVarIdx]
cb [[Sig FreeVarIdx]]
ab : [Sig FreeVarIdx]
restB)
  | [[Sig FreeVarIdx]] -> FreeVarIdx
forall (t :: * -> *) a. Foldable t => t a -> FreeVarIdx
length [[Sig FreeVarIdx]]
aa FreeVarIdx -> FreeVarIdx -> Bool
forall a. Eq a => a -> a -> Bool
== [[Sig FreeVarIdx]] -> FreeVarIdx
forall (t :: * -> *) a. Foldable t => t a -> FreeVarIdx
length [[Sig FreeVarIdx]]
ab
  = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
ca [Sig FreeVarIdx]
cb
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [State Env Bool] -> State Env Bool
checkAnd (([Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool)
-> [[Sig FreeVarIdx]] -> [[Sig FreeVarIdx]] -> [State Env Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [[Sig FreeVarIdx]]
aa [[Sig FreeVarIdx]]
ab)
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
  | Bool
otherwise = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

checkArguments (Tuple [] : [Sig FreeVarIdx]
restA) (Tuple [] : [Sig FreeVarIdx]
restB)
  = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
checkArguments (Tuple ([Sig FreeVarIdx]
a : [[Sig FreeVarIdx]]
as) : [Sig FreeVarIdx]
restA) (Tuple [[Sig FreeVarIdx]]
bs : [Sig FreeVarIdx]
restB)
  | [[Sig FreeVarIdx]] -> FreeVarIdx
forall (t :: * -> *) a. Foldable t => t a -> FreeVarIdx
length [[Sig FreeVarIdx]]
as FreeVarIdx -> FreeVarIdx -> FreeVarIdx
forall a. Num a => a -> a -> a
+ FreeVarIdx
1 FreeVarIdx -> FreeVarIdx -> Bool
forall a. Eq a => a -> a -> Bool
== [[Sig FreeVarIdx]] -> FreeVarIdx
forall (t :: * -> *) a. Foldable t => t a -> FreeVarIdx
length [[Sig FreeVarIdx]]
bs
  , let splits :: [([[Sig FreeVarIdx]], [[Sig FreeVarIdx]])]
splits = [[[Sig FreeVarIdx]]]
-> [[[Sig FreeVarIdx]]]
-> [([[Sig FreeVarIdx]], [[Sig FreeVarIdx]])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([[Sig FreeVarIdx]] -> [[[Sig FreeVarIdx]]]
forall a. [a] -> [[a]]
inits [[Sig FreeVarIdx]]
bs) ([[Sig FreeVarIdx]] -> [[[Sig FreeVarIdx]]]
forall a. [a] -> [[a]]
tails [[Sig FreeVarIdx]]
bs)
        go :: ([[Sig FreeVarIdx]], [[Sig FreeVarIdx]]) -> State Env Bool
go ([[Sig FreeVarIdx]]
i, [Sig FreeVarIdx]
b : [[Sig FreeVarIdx]]
rest)
            = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
a [Sig FreeVarIdx]
b
           State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [[[Sig FreeVarIdx]] -> Sig FreeVarIdx
forall varIx. [[Sig varIx]] -> Sig varIx
Tuple [[Sig FreeVarIdx]]
as] [[[Sig FreeVarIdx]] -> Sig FreeVarIdx
forall varIx. [[Sig varIx]] -> Sig varIx
Tuple ([[Sig FreeVarIdx]] -> Sig FreeVarIdx)
-> [[Sig FreeVarIdx]] -> Sig FreeVarIdx
forall a b. (a -> b) -> a -> b
$ [[Sig FreeVarIdx]]
i [[Sig FreeVarIdx]] -> [[Sig FreeVarIdx]] -> [[Sig FreeVarIdx]]
forall a. [a] -> [a] -> [a]
++ [[Sig FreeVarIdx]]
rest]
           State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB
        go ([[Sig FreeVarIdx]], [[Sig FreeVarIdx]])
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  = [State Env Bool] -> State Env Bool
forall env. [State env Bool] -> State env Bool
checkOr ([State Env Bool] -> State Env Bool)
-> [State Env Bool] -> State Env Bool
forall a b. (a -> b) -> a -> b
$ ([[Sig FreeVarIdx]], [[Sig FreeVarIdx]]) -> State Env Bool
go (([[Sig FreeVarIdx]], [[Sig FreeVarIdx]]) -> State Env Bool)
-> [([[Sig FreeVarIdx]], [[Sig FreeVarIdx]])] -> [State Env Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([[Sig FreeVarIdx]], [[Sig FreeVarIdx]])]
splits
  | Bool
otherwise = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

checkArguments (KindSig [Sig FreeVarIdx]
ta [Sig FreeVarIdx]
ka : [Sig FreeVarIdx]
restA) (KindSig [Sig FreeVarIdx]
tb [Sig FreeVarIdx]
kb : [Sig FreeVarIdx]
restB)
  = [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
ta [Sig FreeVarIdx]
tb
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkMatch [Sig FreeVarIdx]
ka [Sig FreeVarIdx]
kb
 State Env Bool -> State Env Bool -> State Env Bool
forall env. State env Bool -> State env Bool -> State env Bool
/\ [Sig FreeVarIdx] -> [Sig FreeVarIdx] -> State Env Bool
checkArguments [Sig FreeVarIdx]
restA [Sig FreeVarIdx]
restB

checkArguments [Sig FreeVarIdx]
_ [Sig FreeVarIdx]
_ = Bool -> State Env Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False