TypeSig.hs

{-# 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
    { _tsTerm :: h :# term
    , _tsType :: h :# Scheme vars (TypeOf term)
    }
    deriving (Generic)

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

instance
    Constraints (TypeSig vars term h) Pretty =>
    Pretty (TypeSig vars term h)
    where
    pPrintPrec lvl p (TypeSig term typ) =
        pPrintPrec lvl 1 term <+> Pretty.text ":" <+> pPrintPrec lvl 1 typ
            & maybeParens (p > 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 (TypeSig x s) =
        do
            InferredChild xI xR <- inferChild x
            InferredChild sI sR <- inferChild s
            (t, ()) <- instantiateWith (pure ()) USkolem (sR ^. _HFlip)
            xR
                & inferredType (Proxy @term) #%%~ unify t
                <&> (TypeSig xI sI,)
            & localLevel