module Unison.KindInference.Constraint.Unsolved
( Constraint (..),
typeProv,
prov,
loc,
)
where
import Control.Lens (Lens, Lens', Traversal)
import Unison.KindInference.Constraint.Provenance (Provenance)
import Unison.KindInference.Constraint.Provenance qualified as Provenance
data Constraint uv v loc typeProv
=
IsType uv (typeProv v loc)
| IsArr uv (Provenance v loc) uv uv
| IsAbility uv (Provenance v loc)
| Unify (Provenance v loc) uv uv
deriving stock (Int -> Constraint uv v loc typeProv -> ShowS
[Constraint uv v loc typeProv] -> ShowS
Constraint uv v loc typeProv -> String
(Int -> Constraint uv v loc typeProv -> ShowS)
-> (Constraint uv v loc typeProv -> String)
-> ([Constraint uv v loc typeProv] -> ShowS)
-> Show (Constraint uv v loc typeProv)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Int -> Constraint uv v loc typeProv -> ShowS
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
[Constraint uv v loc typeProv] -> ShowS
forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Constraint uv v loc typeProv -> String
$cshowsPrec :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Int -> Constraint uv v loc typeProv -> ShowS
showsPrec :: Int -> Constraint uv v loc typeProv -> ShowS
$cshow :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
Constraint uv v loc typeProv -> String
show :: Constraint uv v loc typeProv -> String
$cshowList :: forall uv v loc (typeProv :: * -> * -> *).
(Show v, Show loc, Show uv, Show (typeProv v loc)) =>
[Constraint uv v loc typeProv] -> ShowS
showList :: [Constraint uv v loc typeProv] -> ShowS
Show, Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
(Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> Eq (Constraint uv v loc typeProv)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c== :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
== :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c/= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Eq loc, Eq uv, Eq (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
/= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
Eq, Eq (Constraint uv v loc typeProv)
Eq (Constraint uv v loc typeProv) =>
(Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv)
-> (Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv)
-> Ord (Constraint uv v loc typeProv)
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Eq (Constraint uv v loc typeProv)
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
$ccompare :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
compare :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Ordering
$c< :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
< :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c<= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
<= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c> :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
> :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$c>= :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
>= :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Bool
$cmax :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
max :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
$cmin :: forall uv v loc (typeProv :: * -> * -> *).
(Var v, Ord loc, Ord uv, Ord (typeProv v loc)) =>
Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
min :: Constraint uv v loc typeProv
-> Constraint uv v loc typeProv -> Constraint uv v loc typeProv
Ord)
typeProv ::
Traversal
(Constraint uv v loc prov)
(Constraint uv v loc prov')
(prov v loc)
(prov' v loc)
typeProv :: forall uv v loc (prov :: * -> * -> *) (prov' :: * -> * -> *)
(f :: * -> *).
Applicative f =>
(prov v loc -> f (prov' v loc))
-> Constraint uv v loc prov -> f (Constraint uv v loc prov')
typeProv prov v loc -> f (prov' v loc)
f = \case
IsType uv
x prov v loc
l -> uv -> prov' v loc -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType uv
x (prov' v loc -> Constraint uv v loc prov')
-> f (prov' v loc) -> f (Constraint uv v loc prov')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> prov v loc -> f (prov' v loc)
f prov v loc
l
IsAbility uv
x Provenance v loc
l -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (uv -> Provenance v loc -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility uv
x Provenance v loc
l)
IsArr uv
s Provenance v loc
l uv
a uv
b -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr uv
s Provenance v loc
l uv
a uv
b)
Unify Provenance v loc
l uv
a uv
b -> Constraint uv v loc prov' -> f (Constraint uv v loc prov')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Provenance v loc -> uv -> uv -> Constraint uv v loc prov'
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify Provenance v loc
l uv
a uv
b)
{-# INLINE typeProv #-}
prov ::
Lens
(Constraint uv v loc Provenance)
(Constraint uv v loc' Provenance)
(Provenance v loc)
(Provenance v loc')
prov :: forall uv v loc loc' (f :: * -> *).
Functor f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc' Provenance)
prov Provenance v loc -> f (Provenance v loc')
f = \case
IsType uv
x Provenance v loc
l -> uv -> Provenance v loc' -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
IsType uv
x (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
IsAbility uv
x Provenance v loc
l -> uv -> Provenance v loc' -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
IsAbility uv
x (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
IsArr uv
s Provenance v loc
l uv
a uv
b -> (\Provenance v loc'
x -> uv
-> Provenance v loc' -> uv -> uv -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
IsArr uv
s Provenance v loc'
x uv
a uv
b) (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
Unify Provenance v loc
l uv
a uv
b -> (\Provenance v loc'
x -> Provenance v loc' -> uv -> uv -> Constraint uv v loc' Provenance
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unify Provenance v loc'
x uv
a uv
b) (Provenance v loc' -> Constraint uv v loc' Provenance)
-> f (Provenance v loc') -> f (Constraint uv v loc' Provenance)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc -> f (Provenance v loc')
f Provenance v loc
l
{-# INLINE prov #-}
loc :: Lens' (Constraint uv v loc Provenance) loc
loc :: forall uv v loc (f :: * -> *).
Functor f =>
(loc -> f loc)
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
loc = (Provenance v loc -> f (Provenance v loc))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
forall uv v loc loc' (f :: * -> *).
Functor f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc' Provenance)
prov ((Provenance v loc -> f (Provenance v loc))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance))
-> ((loc -> f loc) -> Provenance v loc -> f (Provenance v loc))
-> (loc -> f loc)
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
forall v loc (f :: * -> *).
Functor f =>
(loc -> f loc) -> Provenance v loc -> f (Provenance v loc)
Provenance.loc
{-# INLINE loc #-}