{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Infer.Blame
( blame
, Blame (..)
, BlameResult (..)
, _Good
, _Mismatch
, InferOf'
) where
import qualified Control.Lens as Lens
import Control.Monad.Except (MonadError (..))
import Data.List (sortOn)
import Hyper
import Hyper.Class.Infer
import Hyper.Class.Traversable (ContainedH (..))
import Hyper.Class.Unify (UVarOf, UnifyGen)
import Hyper.Infer.Result
import Hyper.Recurse
import Hyper.Unify.New (newUnbound)
import Hyper.Unify.Occurs (occursCheck)
import Hyper.Internal.Prelude
class
(Infer m t, RTraversable t, HTraversable (InferOf t), HPointed (InferOf t)) =>
Blame m t
where
inferOfUnify ::
Proxy t ->
InferOf t # UVarOf m ->
InferOf t # UVarOf m ->
m ()
inferOfMatches ::
Proxy t ->
InferOf t # UVarOf m ->
InferOf t # UVarOf m ->
m Bool
blamableRecursive :: Proxy m -> RecMethod (Blame m) t
{-# INLINE blamableRecursive #-}
default blamableRecursive :: HNodesConstraint t (Blame m) => Proxy m -> RecMethod (Blame m) t
blamableRecursive Proxy m
_ Proxy t
_ = forall (a :: Constraint). a => Dict a
Dict
instance Recursive (Blame m) where
recurse :: forall (h :: HyperType) (proxy :: Constraint -> *).
(HNodes h, Blame m h) =>
proxy (Blame m h) -> Dict (HNodesConstraint h (Blame m))
recurse = forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy m -> RecMethod (Blame m) t
blamableRecursive (forall {k} (t :: k). Proxy t
Proxy @m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (proxy :: Constraint -> *) (f :: HyperType -> Constraint)
(h :: HyperType).
proxy (f h) -> Proxy h
proxyArgument
type InferOf' e v = InferOf (GetHyperType e) # v
prepareH ::
forall m exp a.
Blame m exp =>
Ann a # exp ->
m (Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp)
prepareH :: forall (m :: * -> *) (exp :: HyperType) (a :: HyperType).
Blame m exp =>
(Ann a # exp)
-> m (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
prepareH Ann a # exp
t =
forall (h :: HyperType) (p :: HyperType).
HPointed h =>
(forall (n :: HyperType). HWitness h n -> p # n) -> h # p
hpure (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
f (p h) -> ContainedH f p h
MkContainedH forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound)
forall a b. a -> (a -> b) -> b
& forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) (exp :: HyperType) (a :: HyperType).
Blame m exp =>
(InferOf exp # UVarOf m)
-> (Ann a # exp)
-> m (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
`prepare` Ann a # exp
t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: HyperType) (proxy0 :: (* -> *) -> *)
(proxy1 :: HyperType -> *).
Infer m t =>
proxy0 m
-> proxy1 t
-> Dict
(HNodesConstraint t (Infer m),
HNodesConstraint (InferOf t) (UnifyGen m))
inferContext (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @exp)
prepare ::
forall m exp a.
Blame m exp =>
InferOf exp # UVarOf m ->
Ann a # exp ->
m (Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp)
prepare :: forall (m :: * -> *) (exp :: HyperType) (a :: HyperType).
Blame m exp =>
(InferOf exp # UVarOf m)
-> (Ann a # exp)
-> m (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
prepare InferOf exp # UVarOf m
resFromPosition (Ann a ('AHyperType exp)
a 'AHyperType exp :# Ann a
x) =
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
( forall {k} (t :: k). Proxy t
Proxy @(Blame m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
m (InferredChild (UVarOf m) h t) -> InferChild m h t
InferChild forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
('AHyperType n)
t -> forall (v :: HyperType) (h :: HyperType) (t :: AHyperType).
h t -> (InferOf (GetHyperType t) # v) -> InferredChild v h t
InferredChild Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
('AHyperType n)
t (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
('AHyperType n)
t forall s a. s -> Getting a s a -> a
^. forall (a :: HyperType) (h :: AHyperType). Lens' (Ann a h) (a h)
hAnn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v1 :: HyperType) (e1 :: AHyperType) (v2 :: HyperType)
(e2 :: AHyperType).
Iso
(InferResult v1 e1)
(InferResult v2 e2)
(InferOf (GetHyperType e1) # v1)
(InferOf (GetHyperType e2) # v2)
_InferResult)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (exp :: HyperType) (a :: HyperType).
Blame m exp =>
(Ann a # exp)
-> m (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
prepareH
)
'AHyperType exp :# Ann a
x
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
(proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(Blame m exp))
forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (t :: HyperType) (h :: HyperType).
Infer m t =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferBody
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(exp
# Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
xI, InferOf exp # UVarOf m
r) ->
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann (a ('AHyperType exp)
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (v :: HyperType) (e :: AHyperType).
(InferOf (GetHyperType e) # v) -> InferResult v e
InferResult InferOf exp # UVarOf m
resFromPosition forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (v :: HyperType) (e :: AHyperType).
(InferOf (GetHyperType e) # v) -> InferResult v e
InferResult InferOf exp # UVarOf m
r) exp
# Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
xI
tryUnify ::
forall err m top exp.
(MonadError err m, Blame m exp) =>
HWitness top exp ->
InferOf exp # UVarOf m ->
InferOf exp # UVarOf m ->
m ()
tryUnify :: forall err (m :: * -> *) (top :: HyperType) (exp :: HyperType).
(MonadError err m, Blame m exp) =>
HWitness top exp
-> (InferOf exp # UVarOf m) -> (InferOf exp # UVarOf m) -> m ()
tryUnify HWitness top exp
_ InferOf exp # UVarOf m
i0 InferOf exp # UVarOf m
i1 =
do
forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t -> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m ()
inferOfUnify (forall {k} (t :: k). Proxy t
Proxy @exp) InferOf exp # UVarOf m
i0 InferOf exp # UVarOf m
i1
forall (f :: * -> *) (h :: HyperType) (m :: HyperType).
(Applicative f, HFoldable h) =>
(forall (c :: HyperType). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_ (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m ()
occursCheck) InferOf exp # UVarOf m
i0
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: HyperType) (proxy0 :: (* -> *) -> *)
(proxy1 :: HyperType -> *).
Infer m t =>
proxy0 m
-> proxy1 t
-> Dict
(HNodesConstraint t (Infer m),
HNodesConstraint (InferOf t) (UnifyGen m))
inferContext (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @exp)
forall a b. a -> (a -> b) -> b
& (forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))
data BlameResult v e
= Good (InferOf' e v)
| Mismatch (InferOf' e v, InferOf' e v)
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (v :: HyperType) (e :: AHyperType) x.
Rep (BlameResult v e) x -> BlameResult v e
forall (v :: HyperType) (e :: AHyperType) x.
BlameResult v e -> Rep (BlameResult v e) x
$cto :: forall (v :: HyperType) (e :: AHyperType) x.
Rep (BlameResult v e) x -> BlameResult v e
$cfrom :: forall (v :: HyperType) (e :: AHyperType) x.
BlameResult v e -> Rep (BlameResult v e) x
Generic)
makePrisms ''BlameResult
makeCommonInstances [''BlameResult]
finalize ::
forall a m exp.
Blame m exp =>
Ann (a :*: InferResult (UVarOf m) :*: InferResult (UVarOf m)) # exp ->
m (Ann (a :*: BlameResult (UVarOf m)) # exp)
finalize :: forall (a :: HyperType) (m :: * -> *) (exp :: HyperType).
Blame m exp =>
(Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
-> m (Ann (a :*: BlameResult (UVarOf m)) # exp)
finalize (Ann (a ('AHyperType exp)
a :*: InferResult InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i0 :*: InferResult InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i1) 'AHyperType exp
:# Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
x) =
do
Bool
match <- forall (m :: * -> *) (t :: HyperType).
Blame m t =>
Proxy t
-> (InferOf t # UVarOf m) -> (InferOf t # UVarOf m) -> m Bool
inferOfMatches (forall {k} (t :: k). Proxy t
Proxy @exp) InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i0 InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i1
let result :: BlameResult (UVarOf m) ('AHyperType exp)
result
| Bool
match = forall (v :: HyperType) (e :: AHyperType).
InferOf' e v -> BlameResult v e
Good InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i0
| Bool
otherwise = forall (v :: HyperType) (e :: AHyperType).
(InferOf' e v, InferOf' e v) -> BlameResult v e
Mismatch (InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i0, InferOf (GetHyperType ('AHyperType exp)) # UVarOf m
i1)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (forall {k} (t :: k). Proxy t
Proxy @(Blame m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (a :: HyperType) (m :: * -> *) (exp :: HyperType).
Blame m exp =>
(Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
-> m (Ann (a :*: BlameResult (UVarOf m)) # exp)
finalize) 'AHyperType exp
:# Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
x
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann (a ('AHyperType exp)
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: BlameResult (UVarOf m) ('AHyperType exp)
result)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
(proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(Blame m exp))
blame ::
forall priority err m exp a.
( Ord priority
, MonadError err m
, Blame m exp
) =>
(forall n. a # n -> priority) ->
InferOf exp # UVarOf m ->
Ann a # exp ->
m (Ann (a :*: BlameResult (UVarOf m)) # exp)
blame :: forall priority err (m :: * -> *) (exp :: HyperType)
(a :: HyperType).
(Ord priority, MonadError err m, Blame m exp) =>
(forall (n :: HyperType). (a # n) -> priority)
-> (InferOf exp # UVarOf m)
-> (Ann a # exp)
-> m (Ann (a :*: BlameResult (UVarOf m)) # exp)
blame forall (n :: HyperType). (a # n) -> priority
order InferOf exp # UVarOf m
topLevelType Ann a # exp
e =
do
Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp
p <- forall (m :: * -> *) (exp :: HyperType) (a :: HyperType).
Blame m exp =>
(InferOf exp # UVarOf m)
-> (Ann a # exp)
-> m (Ann
(a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
prepare InferOf exp # UVarOf m
topLevelType Ann a # exp
e
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
( forall {k} (t :: k). Proxy t
Proxy @(Blame m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
\HWitness (HFlip Ann exp) n
w (a ('AHyperType n)
a :*: InferResult InferOf (GetHyperType ('AHyperType n)) # UVarOf m
i0 :*: InferResult InferOf (GetHyperType ('AHyperType n)) # UVarOf m
i1) ->
[(forall (n :: HyperType). (a # n) -> priority
order a ('AHyperType n)
a, forall err (m :: * -> *) (top :: HyperType) (exp :: HyperType).
(MonadError err m, Blame m exp) =>
HWitness top exp
-> (InferOf exp # UVarOf m) -> (InferOf exp # UVarOf m) -> m ()
tryUnify HWitness (HFlip Ann exp) n
w InferOf (GetHyperType ('AHyperType n)) # UVarOf m
i0 InferOf (GetHyperType ('AHyperType n)) # UVarOf m
i1)]
)
(forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
(k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
(k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip forall t b. AReview t b -> b -> t
# Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp
p)
forall a b. a -> (a -> b) -> b
& forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst
forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a b. (a, b) -> b
snd
forall (a :: HyperType) (m :: * -> *) (exp :: HyperType).
Blame m exp =>
(Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp)
-> m (Ann (a :*: BlameResult (UVarOf m)) # exp)
finalize Ann (a :*: (InferResult (UVarOf m) :*: InferResult (UVarOf m)))
# exp
p