module Cryptol.TypeCheck.Default where

import qualified Data.Set as Set
import           Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe(mapMaybe)
import Data.List((\\),nub)
import Control.Monad(guard,mzero)

import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType(tMax)
import Cryptol.TypeCheck.Error(Warning(..), Error(..))
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
import Cryptol.Utils.Panic(panic)

--------------------------------------------------------------------------------

-- | We default constraints of the form @Literal t a@ and @FLiteral m n r a@.
--
--   For @Literal t a@ we examine the context of constraints on the type @a@
--   to decide how to default.  If @Logic a@ is required,
--   we cannot do any defaulting.  Otherwise, we default
--   to either @Integer@ or @Rational@.  In particular, if
--   we need to satisfy the @Field a@, constraint, we choose
--   @Rational@ and otherwise we choose @Integer@.
--
--   For @FLiteral t a@ we always default to @Rational@.
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals [TVar]
as [Goal]
gs = let ([(TVar, Type)]
binds,[Warning]
warns) = [((TVar, Type), Warning)] -> ([(TVar, Type)], [Warning])
forall a b. [(a, b)] -> ([a], [b])
unzip ((TVar -> Maybe ((TVar, Type), Warning))
-> [TVar] -> [((TVar, Type), Warning)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TVar -> Maybe ((TVar, Type), Warning)
tryDefVar [TVar]
as)
                        in ([TVar]
as [TVar] -> [TVar] -> [TVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((TVar, Type) -> TVar) -> [(TVar, Type)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> TVar
forall a b. (a, b) -> a
fst [(TVar, Type)]
binds, [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
binds, [Warning]
warns)
  where
  gSet :: Goals
gSet = [Goal] -> Goals
goalsFromList [Goal]
gs
  allProps :: Set Type
allProps = Goals -> Set Type
saturatedPropSet Goals
gSet
  has :: (Type -> Type) -> TVar -> Bool
has Type -> Type
p TVar
a  = Type -> Set Type -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Type -> Type
p (TVar -> Type
TVar TVar
a)) Set Type
allProps

  tryDefVar :: TVar -> Maybe ((TVar, Type), Warning)
tryDefVar TVar
a =
    -- If there is an `FLiteral` constraint we use that for defaulting.
    case TVar
-> Map TVar (Maybe ((TVar, Type), Warning))
-> Maybe (Maybe ((TVar, Type), Warning))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
a (Goals -> Map TVar (Maybe ((TVar, Type), Warning))
flitDefaultCandidates Goals
gSet) of
      Just Maybe ((TVar, Type), Warning)
m -> Maybe ((TVar, Type), Warning)
m

      -- Otherwise we try to use a `Literal`
      Maybe (Maybe ((TVar, Type), Warning))
Nothing ->
        do Goal
_gt <- TVar -> Map TVar Goal -> Maybe Goal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
a (Goals -> Map TVar Goal
literalGoals Goals
gSet)
           Type
defT <- if (Type -> Type) -> TVar -> Bool
has Type -> Type
pLogic TVar
a then Maybe Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                   else if (Type -> Type) -> TVar -> Bool
has Type -> Type
pField TVar
a Bool -> Bool -> Bool
&& Bool -> Bool
not ((Type -> Type) -> TVar -> Bool
has Type -> Type
pIntegral TVar
a)
                          then Type -> Maybe Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tRational
                   else if Bool -> Bool
not ((Type -> Type) -> TVar -> Bool
has Type -> Type
pField TVar
a) then Type -> Maybe Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tInteger
                   else Maybe Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
           let d :: TVarInfo
d    = TVar -> TVarInfo
tvInfo TVar
a
               w :: Warning
w    = TVarInfo -> Type -> Warning
DefaultingTo TVarInfo
d Type
defT
           Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TVar
a (Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
defT)))  -- Currently shouldn't happen
                                                  -- but future proofing.
           -- XXX: Make sure that `defT` has only variables that `a` is allowed
           -- to depend on
           ((TVar, Type), Warning) -> Maybe ((TVar, Type), Warning)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar
a,Type
defT),Warning
w)


flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar,Type),Warning))
flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Type), Warning))
flitDefaultCandidates Goals
gs =
  [(TVar, Maybe ((TVar, Type), Warning))]
-> Map TVar (Maybe ((TVar, Type), Warning))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Goal -> Maybe (TVar, Maybe ((TVar, Type), Warning)))
-> [Goal] -> [(TVar, Maybe ((TVar, Type), Warning))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Goal -> Maybe (TVar, Maybe ((TVar, Type), Warning))
forall (m :: * -> *).
(Monad m, Alternative m) =>
Goal -> Maybe (TVar, m ((TVar, Type), Warning))
flitCandidate (Set Goal -> [Goal]
forall a. Set a -> [a]
Set.toList (Goals -> Set Goal
goalSet Goals
gs)))
  where
  allProps :: Set Type
allProps = Goals -> Set Type
saturatedPropSet Goals
gs
  has :: (Type -> Type) -> TVar -> Bool
has Type -> Type
p TVar
a  = Type -> Set Type -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Type -> Type
p (TVar -> Type
TVar TVar
a)) Set Type
allProps

  flitCandidate :: Goal -> Maybe (TVar, m ((TVar, Type), Warning))
flitCandidate Goal
g =
    do (Type
_,Type
_,Type
_,Type
x) <- Type -> Maybe (Type, Type, Type, Type)
pIsFLiteral (Goal -> Type
goal Goal
g)
       TVar
a         <- Type -> Maybe TVar
tIsVar Type
x
       (TVar, m ((TVar, Type), Warning))
-> Maybe (TVar, m ((TVar, Type), Warning))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVar
a, do Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ((Type -> Type) -> TVar -> Bool
has Type -> Type
pLogic TVar
a) Bool -> Bool -> Bool
&& Bool -> Bool
not ((Type -> Type) -> TVar -> Bool
has Type -> Type
pIntegral TVar
a))
                   let defT :: Type
defT = Type
tRational
                   let w :: Warning
w    = TVarInfo -> Type -> Warning
DefaultingTo (TVar -> TVarInfo
tvInfo TVar
a) Type
defT
                   ((TVar, Type), Warning) -> m ((TVar, Type), Warning)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((TVar
a,Type
defT),Warning
w))


--------------------------------------------------------------------------------

-- This is what we use to avoid ambiguity when generalizing.

{- If a variable, `a`, is:
    1. Of kind KNum
    2. Generic (i.e., does not appear in the environment)
    3. It appears only in constraints but not in the resulting type
       (i.e., it is not on the RHS of =>)
    4. It (say, the variable 'a') appears only in constraints like this:
        3.1 `a >= t` with (`a` not in `fvs t`)
        3.2 in the `s` of `fin s`

  Then we replace `a` with `max(t1 .. tn)` where the `ts`
  are from the constraints `a >= t`.

  If `t1 .. tn` is empty, then we replace `a` with 0.

  This function assumes that 1-3 have been checked, and implements the rest.
  So, given some variables and constraints that are about to be generalized,
  we return:
      1. a new (same or smaller) set of variables to quantify,
      2. a new set of constraints,
      3. a substitution which indicates what got defaulted.
-}





improveByDefaultingWithPure :: [TVar] -> [Goal] ->
    ( [TVar]    -- non-defaulted
    , [Goal]    -- new constraints
    , Subst     -- improvements from defaulting
    , [Error]   -- width defaulting errors
    )
improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
improveByDefaultingWithPure [TVar]
as [Goal]
ps =
  Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify ([(TVar, ([(Type, Goal)], Set TVar))]
-> Map TVar ([(Type, Goal)], Set TVar)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TVar
a,([],Set TVar
forall a. Set a
Set.empty)) | TVar
a <- [TVar]
as ]) [] [] [Goal]
ps

  where
  -- leq: candidate definitions (i.e. of the form x >= t, x `notElem` fvs t)
  --      for each of these, we keep the list of `t`, and the free vars in them.
  -- fins: all `fin` constraints
  -- others: any other constraints
  classify :: Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others [] =
    let -- First, we use the `leqs` to choose some definitions.
        ([(TVar, Type)]
defs, [Goal]
newOthers)  = [(TVar, Type)]
-> [Goal]
-> Set TVar
-> [(TVar, ([(Type, Goal)], Set TVar))]
-> ([(TVar, Type)], [Goal])
forall b.
TVars b =>
[(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select [] [] ([Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
others) (Map TVar ([(Type, Goal)], Set TVar)
-> [(TVar, ([(Type, Goal)], Set TVar))]
forall k a. Map k a -> [(k, a)]
Map.toList Map TVar ([(Type, Goal)], Set TVar)
leqs)
        su :: Subst
su                 = [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
defs
        names :: Set TVar
names              = Subst -> Set TVar
substBinds Subst
su
        mkErr :: (TVar, Type) -> Error
mkErr (TVar
x,Type
t) =
          case TVar
x of
            TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
d
              | Just Integer
0 <- Type -> Maybe Integer
tIsNum Type
t -> TVarInfo -> Maybe Type -> Error
AmbiguousSize TVarInfo
d Maybe Type
forall a. Maybe a
Nothing
              | Bool
otherwise -> TVarInfo -> Maybe Type -> Error
AmbiguousSize TVarInfo
d (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t)
            TVBound {} -> String -> [String] -> Error
forall a. HasCallStack => String -> [String] -> a
panic String
"Crypto.TypeCheck.Infer"
                 [ String
"tryDefault attempted to default a quantified variable."
                 ]

    in ( [ TVar
a | TVar
a <- [TVar]
as, Bool -> Bool
not (TVar
a TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
names) ]
       , [Goal]
newOthers [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
others [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal] -> [Goal]
forall a. Eq a => [a] -> [a]
nub (Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Goal]
fins)
       , Subst
su
       , ((TVar, Type) -> Error) -> [(TVar, Type)] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> Error
mkErr [(TVar, Type)]
defs
       )


  classify Map TVar ([(Type, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others (Goal
prop : [Goal]
more) =
      case Type -> Type
tNoUser (Goal -> Type
goal Goal
prop) of

        -- We found a `fin` constraint.
        TCon (PC PC
PFin) [ Type
_ ] -> Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
fins) [Goal]
others [Goal]
more

        -- Things of the form: x >= T(x) are not defaulted.
        TCon (PC PC
PGeq) [ TVar TVar
x, Type
t ]
          | TVar
x TVar -> [TVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TVar]
as Bool -> Bool -> Bool
&& TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set TVar
freeRHS ->
           Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs' [Goal]
fins [Goal]
others [Goal]
more
           where freeRHS :: Set TVar
freeRHS = Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t
                 add :: ([a], Set a) -> ([a], Set a) -> ([a], Set a)
add ([a]
xs1,Set a
vs1) ([a]
xs2,Set a
vs2) = ([a]
xs1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
xs2, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
vs1 Set a
vs2)
                 leqs' :: Map TVar ([(Type, Goal)], Set TVar)
leqs' = (([(Type, Goal)], Set TVar)
 -> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar))
-> TVar
-> ([(Type, Goal)], Set TVar)
-> Map TVar ([(Type, Goal)], Set TVar)
-> Map TVar ([(Type, Goal)], Set TVar)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([(Type, Goal)], Set TVar)
-> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar)
forall a a. Ord a => ([a], Set a) -> ([a], Set a) -> ([a], Set a)
add TVar
x ([(Type
t,Goal
prop)],Set TVar
freeRHS) Map TVar ([(Type, Goal)], Set TVar)
leqs

        Type
_ -> Map TVar ([(Type, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Type, Goal)], Set TVar)
leqs [Goal]
fins (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
others) [Goal]
more


  -- Pickout which variables may be defaulted and how.
    -- XXX: simpType t
  select :: [(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select [(TVar, Type)]
yes [b]
no Set TVar
_ [] = ([ (TVar
x, Type
t) | (TVar
x,Type
t) <- [(TVar, Type)]
yes ] ,[b]
no)
  select [(TVar, Type)]
yes [b]
no Set TVar
otherFree ((TVar
x,([(Type, b)]
rhsG,Set TVar
vs)) : [(TVar, ([(Type, b)], Set TVar))]
more) =
    [(TVar, Type)]
-> [b]
-> Set TVar
-> [(TVar, ([(Type, b)], Set TVar))]
-> ([(TVar, Type)], [b])
select [(TVar, Type)]
newYes [b]
newNo Set TVar
newFree [(TVar, ([(Type, b)], Set TVar))]
newMore

    where
    ([Type]
ts,[b]
gs) = [(Type, b)] -> ([Type], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, b)]
rhsG

    -- `x` selected only if appears nowehere else.
    -- this includes other candidates for defaulting.
    ([(TVar, Type)]
newYes,[b]
newNo,Set TVar
newFree,[(TVar, ([(Type, b)], Set TVar))]
newMore)

        -- Mentioned in other constraints, definately not defaultable.
        | TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
otherFree = ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting

        | Bool
otherwise =
            let deps :: [TVar]
deps = [ TVar
y | (TVar
y,([(Type, b)]
_,Set TVar
yvs)) <- [(TVar, ([(Type, b)], Set TVar))]
more, TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
yvs ]
                recs :: [TVar]
recs = (TVar -> Bool) -> [TVar] -> [TVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
vs) [TVar]
deps
            in if Bool -> Bool
not ([TVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TVar]
recs) Bool -> Bool -> Bool
|| TVar -> Bool
isBoundTV TVar
x -- x >= S(y), y >= T(x)
                                 then ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting

                                  -- x >= S,    y >= T(x)   or
                                  -- x >= S(y), y >= S
                                  else ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
yesDefaulting

        where
        noDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
noDefaulting = ( [(TVar, Type)]
yes, [b]
gs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
no, Set TVar
vs Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set TVar
otherFree, [(TVar, ([(Type, b)], Set TVar))]
more )

        yesDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
yesDefaulting =
          let ty :: Type
ty  = case [Type]
ts of
                      [] -> Int -> Type
forall a. Integral a => a -> Type
tNum (Int
0::Int)
                      [Type]
_  -> (Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
tMax [Type]
ts
              su1 :: Subst
su1 = TVar -> Type -> Subst
uncheckedSingleSubst TVar
x Type
ty
          in ( (TVar
x,Type
ty) (TVar, Type) -> [(TVar, Type)] -> [(TVar, Type)]
forall a. a -> [a] -> [a]
: [ (TVar
y,Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 Type
t) | (TVar
y,Type
t) <- [(TVar, Type)]
yes ]
             , [b]
no         -- We know that `x` does not appear here
             , Set TVar
otherFree  -- We know that `x` did not appear here either

             -- No need to update the `vs` because we've already
             -- checked that there are no recursive dependencies.
             , [ (TVar
y, (Subst -> [(Type, b)] -> [(Type, b)]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [(Type, b)]
ts1, Set TVar
vs1)) | (TVar
y,([(Type, b)]
ts1,Set TVar
vs1)) <- [(TVar, ([(Type, b)], Set TVar))]
more ]
             )


{- | Try to pick a reasonable instantiation for an expression with
the given type.  This is useful when we do evaluation at the REPL.
The resulting types should satisfy the constraints of the schema.
The parameters should be all of numeric kind, and the props should als
be numeric -}
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [ (TParam,Type) ])
defaultReplExpr' :: Solver -> [TParam] -> [Type] -> IO (Maybe [(TParam, Type)])
defaultReplExpr' Solver
sol [TParam]
as [Type]
props =
  do let params :: [TVar]
params = (TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as
     Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
params [Type]
props
     case Maybe [(TVar, Nat')]
mb of
       Maybe [(TVar, Nat')]
Nothing -> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TParam, Type)]
forall a. Maybe a
Nothing
       Just [(TVar, Nat')]
mdl0 ->
         do [(TVar, Nat')]
mdl <- Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel Solver
sol [TVar]
params [Type]
props [(TVar, Nat')]
mdl0
            let su :: Subst
su = [(TVar, Type)] -> Subst
listSubst [ (TVar
x, Nat' -> Type
tNat' Nat'
n) | (TVar
x,Nat'
n) <- [(TVar, Nat')]
mdl ]
            Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)]))
-> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
forall a b. (a -> b) -> a -> b
$
              do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
props)))
                 [Type]
tys <- (TVar -> Maybe Type) -> [TVar] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Subst -> TVar -> Maybe Type
forall (m :: * -> *).
(Monad m, Alternative m) =>
Subst -> TVar -> m Type
bindParam Subst
su) [TVar]
params
                 [(TParam, Type)] -> Maybe [(TParam, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Type] -> [(TParam, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
as [Type]
tys)
  where
  bindParam :: Subst -> TVar -> m Type
bindParam Subst
su TVar
tp =
    do let ty :: Type
ty  = TVar -> Type
TVar TVar
tp
           ty' :: Type
ty' = Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
ty
       Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ty')
       Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty'