-- | Functions relating to skolemization used during typechecking
module Language.PureScript.TypeChecker.Skolems
  ( newSkolemConstant
  , introduceSkolemScope
  , newSkolemScope
  , skolemize
  , skolemizeTypesInValue
  , skolemEscapeCheck
  ) where

import Prelude

import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets, modify)
import Data.Foldable (traverse_)
import Data.Functor.Identity (Identity(), runIdentity)
import Data.Set (Set, fromList, notMember)
import Data.Text (Text)
import Language.PureScript.AST (Binder(..), ErrorMessageHint(..), Expr(..), SourceAnn, SourceSpan, everythingWithContextOnValues, everywhereWithContextOnValuesM, nonEmptySpan)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), positionedError, singleError)
import Language.PureScript.Traversals (defS)
import Language.PureScript.TypeChecker.Monad (CheckState(..))
import Language.PureScript.Types (SkolemScope(..), SourceType, Type(..), everythingOnTypes, everywhereOnTypesM, replaceTypeVars)

-- | Generate a new skolem constant
newSkolemConstant :: MonadState CheckState m => m Int
newSkolemConstant :: forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant = do
  Int
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextSkolem
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextSkolem :: Int
checkNextSkolem = Int
s forall a. Num a => a -> a -> a
+ Int
1 }
  forall (m :: * -> *) a. Monad m => a -> m a
return Int
s

-- | Introduce skolem scope at every occurrence of a ForAll
introduceSkolemScope :: MonadState CheckState m => Type a -> m (Type a)
introduceSkolemScope :: forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
go
  where
  go :: Type a -> f (Type a)
go (ForAll a
ann Text
ident Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
Nothing) = forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann Text
ident Maybe (Type a)
mbK Type a
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope)
  go Type a
other = forall (m :: * -> *) a. Monad m => a -> m a
return Type a
other

-- | Generate a new skolem scope
newSkolemScope :: MonadState CheckState m => m SkolemScope
newSkolemScope :: forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope = do
  Int
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextSkolemScope
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextSkolemScope :: Int
checkNextSkolemScope = Int
s forall a. Num a => a -> a -> a
+ Int
1 }
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> SkolemScope
SkolemScope Int
s

-- | Skolemize a type variable by replacing its instances with fresh skolem constants
skolemize :: a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize :: forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize a
ann Text
ident Maybe (Type a)
mbK Int
sko SkolemScope
scope = forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident (forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
ann Text
ident Maybe (Type a)
mbK Int
sko SkolemScope
scope)

-- | This function skolemizes type variables appearing in any type signatures or
-- 'DeferredDictionary' placeholders. These type variables are the only places
-- where scoped type variables can appear in expressions.
skolemizeTypesInValue :: SourceAnn -> Text -> Maybe SourceType -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue :: SourceAnn
-> Text -> Maybe SourceType -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope =
    forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Identity Expr
onExpr'
  where
    onExpr' :: Expr -> Identity Expr
    (Declaration -> Identity Declaration
_, Expr -> Identity Expr
onExpr', Binder -> Identity Binder
_, CaseAlternative -> Identity CaseAlternative
_, DoNotationElement -> Identity DoNotationElement
_, Guard -> Identity Guard
_) = forall (m :: * -> *) s.
Monad m =>
s
-> (s -> Declaration -> m (s, Declaration))
-> (s -> Expr -> m (s, Expr))
-> (s -> Binder -> m (s, Binder))
-> (s -> CaseAlternative -> m (s, CaseAlternative))
-> (s -> DoNotationElement -> m (s, DoNotationElement))
-> (s -> Guard -> m (s, Guard))
-> (Declaration -> m Declaration, Expr -> m Expr,
    Binder -> m Binder, CaseAlternative -> m CaseAlternative,
    DoNotationElement -> m DoNotationElement, Guard -> m Guard)
everywhereWithContextOnValuesM [] forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS [Text] -> Expr -> Identity ([Text], Expr)
onExpr [Text] -> Binder -> Identity ([Text], Binder)
onBinder forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS

    onExpr :: [Text] -> Expr -> Identity ([Text], Expr)
    onExpr :: [Text] -> Expr -> Identity ([Text], Expr)
onExpr [Text]
sco (DeferredDictionary Qualified (ProperName 'ClassName)
c [SourceType]
ts)
      | Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Qualified (ProperName 'ClassName) -> [SourceType] -> Expr
DeferredDictionary Qualified (ProperName 'ClassName)
c (forall a b. (a -> b) -> [a] -> [b]
map (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope) [SourceType]
ts))
    onExpr [Text]
sco (TypedValue Bool
check Expr
val SourceType
ty)
      | Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco forall a. [a] -> [a] -> [a]
++ SourceType -> [Text]
peelTypeVars SourceType
ty, Bool -> Expr -> SourceType -> Expr
TypedValue Bool
check Expr
val (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty))
    onExpr [Text]
sco Expr
other = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Expr
other)

    onBinder :: [Text] -> Binder -> Identity ([Text], Binder)
    onBinder :: [Text] -> Binder -> Identity ([Text], Binder)
onBinder [Text]
sco (TypedBinder SourceType
ty Binder
b)
      | Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco forall a. [a] -> [a] -> [a]
++ SourceType -> [Text]
peelTypeVars SourceType
ty, SourceType -> Binder -> Binder
TypedBinder (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty) Binder
b)
    onBinder [Text]
sco Binder
other = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Binder
other)

    peelTypeVars :: SourceType -> [Text]
    peelTypeVars :: SourceType -> [Text]
peelTypeVars (ForAll SourceAnn
_ Text
i Maybe SourceType
_ SourceType
ty Maybe SkolemScope
_) = Text
i forall a. a -> [a] -> [a]
: SourceType -> [Text]
peelTypeVars SourceType
ty
    peelTypeVars SourceType
_ = []

-- | Ensure skolem variables do not escape their scope
--
-- Every skolem variable is created when a 'ForAll' type is skolemized.
-- This determines the scope of that skolem variable, which is copied from
-- the 'SkolemScope' field of the 'ForAll' constructor.
--
-- This function traverses the tree top-down, and collects any 'SkolemScope's
-- introduced by 'ForAll's. If a 'Skolem' is encountered whose 'SkolemScope' is
-- not in the current list, then we have found an escaped skolem variable.
skolemEscapeCheck :: MonadError MultipleErrors m => Expr -> m ()
skolemEscapeCheck :: forall (m :: * -> *). MonadError MultipleErrors m => Expr -> m ()
skolemEscapeCheck (TypedValue Bool
False Expr
_ SourceType
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
skolemEscapeCheck expr :: Expr
expr@TypedValue{} =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorMessage -> MultipleErrors
singleError) (Expr -> [ErrorMessage]
toSkolemErrors Expr
expr)
  where
    toSkolemErrors :: Expr -> [ErrorMessage]
    (Declaration -> [ErrorMessage]
_, Expr -> [ErrorMessage]
toSkolemErrors, Binder -> [ErrorMessage]
_, CaseAlternative -> [ErrorMessage]
_, DoNotationElement -> [ErrorMessage]
_) = forall s r.
s
-> r
-> (r -> r -> r)
-> (s -> Declaration -> (s, r))
-> (s -> Expr -> (s, r))
-> (s -> Binder -> (s, r))
-> (s -> CaseAlternative -> (s, r))
-> (s -> DoNotationElement -> (s, r))
-> (Declaration -> r, Expr -> r, Binder -> r, CaseAlternative -> r,
    DoNotationElement -> r)
everythingWithContextOnValues (forall a. Monoid a => a
mempty, forall a. Maybe a
Nothing) [] forall a. Semigroup a => a -> a -> a
(<>) forall {a} {p} {a}. a -> p -> (a, [a])
def (Set SkolemScope, Maybe SourceSpan)
-> Expr -> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
go forall {a} {p} {a}. a -> p -> (a, [a])
def forall {a} {p} {a}. a -> p -> (a, [a])
def forall {a} {p} {a}. a -> p -> (a, [a])
def

    def :: a -> p -> (a, [a])
def a
s p
_ = (a
s, [])

    go :: (Set SkolemScope, Maybe SourceSpan)
       -> Expr
       -> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
    go :: (Set SkolemScope, Maybe SourceSpan)
-> Expr -> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
go (Set SkolemScope
scopes, Maybe SourceSpan
_) (PositionedValue SourceSpan
ss [Comment]
_ Expr
_) = ((Set SkolemScope
scopes, forall a. a -> Maybe a
Just SourceSpan
ss), [])
    go (Set SkolemScope
scopes, Maybe SourceSpan
ssUsed) val :: Expr
val@(TypedValue Bool
_ Expr
_ SourceType
ty) =
        ( (Set SkolemScope
allScopes, Maybe SourceSpan
ssUsed)
        , [ [ErrorMessageHint] -> SimpleErrorMessage -> ErrorMessage
ErrorMessage (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> ErrorMessageHint
positionedError) Maybe SourceSpan
ssUsed [ Expr -> ErrorMessageHint
ErrorInExpression Expr
val ]) forall a b. (a -> b) -> a -> b
$
              Text -> Maybe SourceSpan -> SourceType -> SimpleErrorMessage
EscapedSkolem Text
name (SourceAnn -> Maybe SourceSpan
nonEmptySpan SourceAnn
ssBound) SourceType
ty
          | (SourceAnn
ssBound, Text
name, SkolemScope
scope) <- SourceType -> [(SourceAnn, Text, SkolemScope)]
collectSkolems SourceType
ty
          , forall a. Ord a => a -> Set a -> Bool
notMember SkolemScope
scope Set SkolemScope
allScopes
          ]
        )
      where
        -- Any new skolem scopes introduced by universal quantifiers
        newScopes :: [SkolemScope]
        newScopes :: [SkolemScope]
newScopes = SourceType -> [SkolemScope]
collectScopes SourceType
ty

        -- All scopes, including new scopes
        allScopes :: Set SkolemScope
        allScopes :: Set SkolemScope
allScopes = forall a. Ord a => [a] -> Set a
fromList [SkolemScope]
newScopes forall a. Semigroup a => a -> a -> a
<> Set SkolemScope
scopes

        -- Collect any scopes appearing in quantifiers at the top level
        collectScopes :: SourceType -> [SkolemScope]
        collectScopes :: SourceType -> [SkolemScope]
collectScopes (ForAll SourceAnn
_ Text
_ Maybe SourceType
_ SourceType
t (Just SkolemScope
sco)) = SkolemScope
sco forall a. a -> [a] -> [a]
: SourceType -> [SkolemScope]
collectScopes SourceType
t
        collectScopes ForAll{} = forall a. HasCallStack => String -> a
internalError String
"skolemEscapeCheck: No skolem scope"
        collectScopes SourceType
_ = []

        -- Collect any skolem variables appearing in a type
        collectSkolems :: SourceType -> [(SourceAnn, Text, SkolemScope)]
        collectSkolems :: SourceType -> [(SourceAnn, Text, SkolemScope)]
collectSkolems = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes forall a. [a] -> [a] -> [a]
(++) forall {a}. Type a -> [(a, Text, SkolemScope)]
collect where
          collect :: Type a -> [(a, Text, SkolemScope)]
collect (Skolem a
ss Text
name Maybe (Type a)
_ Int
_ SkolemScope
scope) = [(a
ss, Text
name, SkolemScope
scope)]
          collect Type a
_ = []
    go (Set SkolemScope, Maybe SourceSpan)
scos Expr
_ = ((Set SkolemScope, Maybe SourceSpan)
scos, [])
skolemEscapeCheck Expr
_ = forall a. HasCallStack => String -> a
internalError String
"skolemEscapeCheck: untyped value"