-- | 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
import Language.PureScript.Crash
import Language.PureScript.Errors
import Language.PureScript.Traversals (defS)
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.Types

-- | 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"