{-# LANGUAGE Safe #-}
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, isJust)
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)
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
defaultLiterals [TVar]
as [Goal]
gs = let ([(TVar, Prop)]
binds,[Warning]
warns) = [((TVar, Prop), Warning)] -> ([(TVar, Prop)], [Warning])
forall a b. [(a, b)] -> ([a], [b])
unzip ((TVar -> Maybe ((TVar, Prop), Warning))
-> [TVar] -> [((TVar, Prop), Warning)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TVar -> Maybe ((TVar, Prop), Warning)
tryDefVar [TVar]
as)
in ([TVar]
as [TVar] -> [TVar] -> [TVar]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((TVar, Prop) -> TVar) -> [(TVar, Prop)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Prop) -> TVar
forall a b. (a, b) -> a
fst [(TVar, Prop)]
binds, [(TVar, Prop)] -> Subst
listSubst [(TVar, Prop)]
binds, [Warning]
warns)
where
gSet :: Goals
gSet = [Goal] -> Goals
goalsFromList [Goal]
gs
allProps :: Set Prop
allProps = Goals -> Set Prop
saturatedPropSet Goals
gSet
has :: (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
p TVar
a = Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Prop -> Prop
p (TVar -> Prop
TVar TVar
a)) Set Prop
allProps
isLiteralGoal :: TVar -> Bool
isLiteralGoal TVar
a = Maybe Goal -> Bool
forall a. Maybe a -> Bool
isJust (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)) Bool -> Bool -> Bool
||
Maybe Goal -> Bool
forall a. Maybe a -> Bool
isJust (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
literalLessThanGoals Goals
gSet))
tryDefVar :: TVar -> Maybe ((TVar, Prop), Warning)
tryDefVar TVar
a =
case TVar
-> Map TVar (Maybe ((TVar, Prop), Warning))
-> Maybe (Maybe ((TVar, Prop), Warning))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
a (Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
flitDefaultCandidates Goals
gSet) of
Just Maybe ((TVar, Prop), Warning)
m -> Maybe ((TVar, Prop), Warning)
m
Maybe (Maybe ((TVar, Prop), Warning))
Nothing
| TVar -> Bool
isLiteralGoal TVar
a -> do
Prop
defT <- if (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pLogic TVar
a then Maybe Prop
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
else if (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pField TVar
a Bool -> Bool -> Bool
&& Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pIntegral TVar
a)
then Prop -> Maybe Prop
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
tRational
else if Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pField TVar
a) then Prop -> Maybe Prop
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
tInteger
else Maybe Prop
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
let d :: TVarInfo
d = TVar -> TVarInfo
tvInfo TVar
a
w :: Warning
w = TVarInfo -> Prop -> Warning
DefaultingTo TVarInfo
d Prop
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 (Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
defT)))
((TVar, Prop), Warning) -> Maybe ((TVar, Prop), Warning)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar
a,Prop
defT),Warning
w)
| Bool
otherwise -> Maybe ((TVar, Prop), Warning)
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar,Type),Warning))
flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
flitDefaultCandidates Goals
gs =
[(TVar, Maybe ((TVar, Prop), Warning))]
-> Map TVar (Maybe ((TVar, Prop), Warning))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning)))
-> [Goal] -> [(TVar, Maybe ((TVar, Prop), Warning))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning))
forall {m :: * -> *}.
(Monad m, Alternative m) =>
Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
flitCandidate (Set Goal -> [Goal]
forall a. Set a -> [a]
Set.toList (Goals -> Set Goal
goalSet Goals
gs)))
where
allProps :: Set Prop
allProps = Goals -> Set Prop
saturatedPropSet Goals
gs
has :: (Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
p TVar
a = Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Prop -> Prop
p (TVar -> Prop
TVar TVar
a)) Set Prop
allProps
flitCandidate :: Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
flitCandidate Goal
g =
do (Prop
_,Prop
_,Prop
_,Prop
x) <- Prop -> Maybe (Prop, Prop, Prop, Prop)
pIsFLiteral (Goal -> Prop
goal Goal
g)
TVar
a <- Prop -> Maybe TVar
tIsVar Prop
x
(TVar, m ((TVar, Prop), Warning))
-> Maybe (TVar, m ((TVar, Prop), Warning))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TVar
a, do Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pLogic TVar
a) Bool -> Bool -> Bool
&& Bool -> Bool
not ((Prop -> Prop) -> TVar -> Bool
has Prop -> Prop
pIntegral TVar
a))
let defT :: Prop
defT = Prop
tRational
let w :: Warning
w = TVarInfo -> Prop -> Warning
DefaultingTo (TVar -> TVarInfo
tvInfo TVar
a) Prop
defT
((TVar, Prop), Warning) -> m ((TVar, Prop), Warning)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((TVar
a,Prop
defT),Warning
w))
improveByDefaultingWithPure :: [TVar] -> [Goal] ->
( [TVar]
, [Goal]
, Subst
, [Error]
)
improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
improveByDefaultingWithPure [TVar]
as [Goal]
ps =
Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify ([(TVar, ([(Prop, Goal)], Set TVar))]
-> Map TVar ([(Prop, 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
classify :: Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others [] =
let
([(TVar, Prop)]
defs, [Goal]
newOthers) = [(TVar, Prop)]
-> [Goal]
-> Set TVar
-> [(TVar, ([(Prop, Goal)], Set TVar))]
-> ([(TVar, Prop)], [Goal])
forall {b}.
TVars b =>
[(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [] [] ([Goal] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Goal]
others) (Map TVar ([(Prop, Goal)], Set TVar)
-> [(TVar, ([(Prop, Goal)], Set TVar))]
forall k a. Map k a -> [(k, a)]
Map.toList Map TVar ([(Prop, Goal)], Set TVar)
leqs)
su :: Subst
su = [(TVar, Prop)] -> Subst
listSubst [(TVar, Prop)]
defs
names :: Set TVar
names = Subst -> Set TVar
substBinds Subst
su
mkErr :: (TVar, Prop) -> Error
mkErr (TVar
x,Prop
t) =
case TVar
x of
TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
d
| Just Integer
0 <- Prop -> Maybe Integer
tIsNum Prop
t -> TVarInfo -> Maybe Prop -> Error
AmbiguousSize TVarInfo
d Maybe Prop
forall a. Maybe a
Nothing
| Bool
otherwise -> TVarInfo -> Maybe Prop -> Error
AmbiguousSize TVarInfo
d (Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
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, Prop) -> Error) -> [(TVar, Prop)] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Prop) -> Error
mkErr [(TVar, Prop)]
defs
)
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins [Goal]
others (Goal
prop : [Goal]
more) =
case Prop -> Prop
tNoUser (Goal -> Prop
goal Goal
prop) of
TCon (PC PC
PFin) [ Prop
_ ] -> Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
fins) [Goal]
others [Goal]
more
TCon (PC PC
PGeq) [ TVar TVar
x, Prop
t ]
| TVar
x TVar -> [TVar] -> Bool
forall a. Eq a => a -> [a] -> 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 ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs' [Goal]
fins [Goal]
others [Goal]
more
where freeRHS :: Set TVar
freeRHS = Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Prop
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 ([(Prop, Goal)], Set TVar)
leqs' = (([(Prop, Goal)], Set TVar)
-> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar))
-> TVar
-> ([(Prop, Goal)], Set TVar)
-> Map TVar ([(Prop, Goal)], Set TVar)
-> Map TVar ([(Prop, Goal)], Set TVar)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([(Prop, Goal)], Set TVar)
-> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar)
forall {a} {a}.
Ord a =>
([a], Set a) -> ([a], Set a) -> ([a], Set a)
add TVar
x ([(Prop
t,Goal
prop)],Set TVar
freeRHS) Map TVar ([(Prop, Goal)], Set TVar)
leqs
Prop
_ -> Map TVar ([(Prop, Goal)], Set TVar)
-> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
classify Map TVar ([(Prop, Goal)], Set TVar)
leqs [Goal]
fins (Goal
prop Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
: [Goal]
others) [Goal]
more
select :: [(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [(TVar, Prop)]
yes [b]
no Set TVar
_ [] = ([ (TVar
x, Prop
t) | (TVar
x,Prop
t) <- [(TVar, Prop)]
yes ] ,[b]
no)
select [(TVar, Prop)]
yes [b]
no Set TVar
otherFree ((TVar
x,([(Prop, b)]
rhsG,Set TVar
vs)) : [(TVar, ([(Prop, b)], Set TVar))]
more) =
[(TVar, Prop)]
-> [b]
-> Set TVar
-> [(TVar, ([(Prop, b)], Set TVar))]
-> ([(TVar, Prop)], [b])
select [(TVar, Prop)]
newYes [b]
newNo Set TVar
newFree [(TVar, ([(Prop, b)], Set TVar))]
newMore
where
([Prop]
ts,[b]
gs) = [(Prop, b)] -> ([Prop], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Prop, b)]
rhsG
([(TVar, Prop)]
newYes,[b]
newNo,Set TVar
newFree,[(TVar, ([(Prop, b)], Set TVar))]
newMore)
| TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
otherFree = ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting
| Bool
otherwise =
let deps :: [TVar]
deps = [ TVar
y | (TVar
y,([(Prop, b)]
_,Set TVar
yvs)) <- [(TVar, ([(Prop, 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TVar]
recs) Bool -> Bool -> Bool
|| TVar -> Bool
isBoundTV TVar
x
then ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting
else ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
yesDefaulting
where
noDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
noDefaulting = ( [(TVar, Prop)]
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, ([(Prop, b)], Set TVar))]
more )
yesDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
yesDefaulting =
let ty :: Prop
ty = case [Prop]
ts of
[] -> Int -> Prop
forall a. Integral a => a -> Prop
tNum (Int
0::Int)
[Prop]
_ -> (Prop -> Prop -> Prop) -> [Prop] -> Prop
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Prop -> Prop -> Prop
tMax [Prop]
ts
su1 :: Subst
su1 = TVar -> Prop -> Subst
uncheckedSingleSubst TVar
x Prop
ty
in ( (TVar
x,Prop
ty) (TVar, Prop) -> [(TVar, Prop)] -> [(TVar, Prop)]
forall a. a -> [a] -> [a]
: [ (TVar
y,Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 Prop
t) | (TVar
y,Prop
t) <- [(TVar, Prop)]
yes ]
, [b]
no
, Set TVar
otherFree
, [ (TVar
y, (Subst -> [(Prop, b)] -> [(Prop, b)]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su1 [(Prop, b)]
ts1, Set TVar
vs1)) | (TVar
y,([(Prop, b)]
ts1,Set TVar
vs1)) <- [(TVar, ([(Prop, b)], Set TVar))]
more ]
)
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [ (TParam,Type) ])
defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Prop)])
defaultReplExpr' Solver
sol [TParam]
as [Prop]
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] -> [Prop] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
params [Prop]
props
case Maybe [(TVar, Nat')]
mb of
Maybe [(TVar, Nat')]
Nothing -> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TParam, Prop)]
forall a. Maybe a
Nothing
Just [(TVar, Nat')]
mdl0 ->
do [(TVar, Nat')]
mdl <- Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel Solver
sol [TVar]
params [Prop]
props [(TVar, Nat')]
mdl0
let su :: Subst
su = [(TVar, Prop)] -> Subst
listSubst [ (TVar
x, Nat' -> Prop
tNat' Nat'
n) | (TVar
x,Nat'
n) <- [(TVar, Nat')]
mdl ]
Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)]))
-> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
forall a b. (a -> b) -> a -> b
$
do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Prop] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Prop]
props)))
[Prop]
tys <- (TVar -> Maybe Prop) -> [TVar] -> Maybe [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Subst -> TVar -> Maybe Prop
forall {m :: * -> *}.
(Monad m, Alternative m) =>
Subst -> TVar -> m Prop
bindParam Subst
su) [TVar]
params
[(TParam, Prop)] -> Maybe [(TParam, Prop)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TParam] -> [Prop] -> [(TParam, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
as [Prop]
tys)
where
bindParam :: Subst -> TVar -> m Prop
bindParam Subst
su TVar
tp =
do let ty :: Prop
ty = TVar -> Prop
TVar TVar
tp
ty' :: Prop
ty' = Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
ty
Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Prop
ty Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
/= Prop
ty')
Prop -> m Prop
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
ty'