{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Type signatures
module Hyper.Syntax.TypeSig
    ( TypeSig (..)
    , tsType
    , tsTerm
    , W_TypeSig (..)
    ) where

import Generics.Constraints (Constraints)
import Hyper
import Hyper.Infer
import Hyper.Syntax.Scheme
import Hyper.Unify (UnifyGen, unify)
import Hyper.Unify.Generalize (instantiateWith)
import Hyper.Unify.Term (UTerm (..))
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)

import Hyper.Internal.Prelude

data TypeSig vars term h = TypeSig
    { forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType).
TypeSig vars term h -> h :# term
_tsTerm :: h :# term
    , forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType).
TypeSig vars term h -> h :# Scheme vars (TypeOf term)
_tsType :: h :# Scheme vars (TypeOf term)
    }
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
$cto :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
$cfrom :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
Generic)

makeLenses ''TypeSig
makeCommonInstances [''TypeSig]
makeHTraversableApplyAndBases ''TypeSig

instance
    Constraints (TypeSig vars term h) Pretty =>
    Pretty (TypeSig vars term h)
    where
    pPrintPrec :: PrettyLevel -> Rational -> TypeSig vars term h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (TypeSig GetHyperType h ('AHyperType term)
term GetHyperType h ('AHyperType (Scheme vars (TypeOf term)))
typ) =
        forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 GetHyperType h ('AHyperType term)
term Doc -> Doc -> Doc
<+> String -> Doc
Pretty.text String
":" Doc -> Doc -> Doc
<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 GetHyperType h ('AHyperType (Scheme vars (TypeOf term)))
typ
            forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
1)

type instance InferOf (TypeSig _ t) = InferOf t

instance
    ( MonadScopeLevel m
    , HasInferredType term
    , HasInferredValue (TypeOf term)
    , HTraversable vars
    , HTraversable (InferOf term)
    , HNodesConstraint (InferOf term) (UnifyGen m)
    , HNodesConstraint vars (MonadInstantiate m)
    , UnifyGen m (TypeOf term)
    , Infer m (TypeOf term)
    , Infer m term
    ) =>
    Infer m (TypeSig vars term)
    where
    inferBody :: forall (h :: AHyperType -> *).
(TypeSig vars term # InferChild m h)
-> m (TypeSig vars term # h,
      InferOf (TypeSig vars term) # UVarOf m)
inferBody (TypeSig 'AHyperType (InferChild m h) :# term
x 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
s) =
        do
            InferredChild h ('AHyperType term)
xI InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR <- forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# term
x
            InferredChild h ('AHyperType (Scheme vars (TypeOf term)))
sI InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR <- forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
s
            (UVarOf m # TypeOf term
t, ()) <- forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR forall s a. s -> Getting a s a -> a
^. forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip)
            InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR
                forall a b. a -> (a -> b) -> b
& forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (forall {k} (t :: k). Proxy t
Proxy @term) forall (f :: * -> *) s t a b.
Functor f =>
ALens s t a b -> (a -> f b) -> s -> f t
#%%~ forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify UVarOf m # TypeOf term
t
                forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType).
(h :# term)
-> (h :# Scheme vars (TypeOf term)) -> TypeSig vars term h
TypeSig h ('AHyperType term)
xI h ('AHyperType (Scheme vars (TypeOf term)))
sI,)
            forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel