{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- For 'Ord IntVar' instance

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Type inference for the Swarm language.  For the approach used here,
-- see
-- https://byorgey.wordpress.com/2021/09/08/implementing-hindley-milner-with-the-unification-fd-library/ .
module Swarm.Language.Typecheck (
  -- * Type errors
  ContextualTypeErr (..),
  TypeErr (..),
  InvalidAtomicReason (..),

  -- * Type provenance
  Source (..),
  withSource,
  Join,
  getJoin,

  -- * Typechecking stack
  TCFrame (..),
  LocatedTCFrame (..),
  TCStack,
  withFrame,
  getTCStack,

  -- * Typechecking monad
  TC,
  runTC,
  fresh,

  -- * Unification
  substU,
  unify,
  HasBindings (..),
  instantiate,
  skolemize,
  generalize,

  -- * Type inference
  inferTop,
  inferModule,
  infer,
  inferConst,
  check,
  isSimpleUType,
) where

import Control.Arrow ((***))
import Control.Category ((>>>))
import Control.Lens ((^.))
import Control.Lens.Indexed (itraverse)
import Control.Monad (forM_, void, when, (<=<))
import Control.Monad.Except (
  ExceptT,
  MonadError (catchError, throwError),
  runExceptT,
 )
import Control.Monad.Reader (
  MonadReader (ask, local),
  ReaderT (runReaderT),
  mapReaderT,
 )
import Control.Monad.Trans.Class (MonadTrans (lift))
import Control.Unification hiding (applyBindings, unify, (=:=))
import Control.Unification qualified as U
import Control.Unification.IntVar
import Data.Data (Data, gmapM)
import Data.Foldable (fold)
import Data.Functor.Identity
import Data.Generics (mkM)
import Data.Map (Map, (!))
import Data.Map qualified as M
import Data.Maybe
import Data.Set (Set, (\\))
import Data.Set qualified as S
import Data.Text qualified as T
import Swarm.Language.Context hiding (lookup)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Module
import Swarm.Language.Parse.QQ (tyQ)
import Swarm.Language.Syntax
import Swarm.Language.Typecheck.Unify
import Swarm.Language.Types
import Prelude hiding (lookup)

------------------------------------------------------------
-- Typechecking stack

-- | A frame to keep track of something we were in the middle of doing
--   during typechecking.
data TCFrame where
  -- | Checking a definition.
  TCDef :: Var -> TCFrame
  -- | Inferring the LHS of a bind.
  TCBindL :: TCFrame
  -- | Inferring the RHS of a bind.
  TCBindR :: TCFrame
  deriving (Int -> TCFrame -> ShowS
[TCFrame] -> ShowS
TCFrame -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCFrame] -> ShowS
$cshowList :: [TCFrame] -> ShowS
show :: TCFrame -> String
$cshow :: TCFrame -> String
showsPrec :: Int -> TCFrame -> ShowS
$cshowsPrec :: Int -> TCFrame -> ShowS
Show)

-- | A typechecking stack frame together with the relevant @SrcLoc@.
data LocatedTCFrame = LocatedTCFrame SrcLoc TCFrame
  deriving (Int -> LocatedTCFrame -> ShowS
TCStack -> ShowS
LocatedTCFrame -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: TCStack -> ShowS
$cshowList :: TCStack -> ShowS
show :: LocatedTCFrame -> String
$cshow :: LocatedTCFrame -> String
showsPrec :: Int -> LocatedTCFrame -> ShowS
$cshowsPrec :: Int -> LocatedTCFrame -> ShowS
Show)

-- | A typechecking stack keeps track of what we are currently in the
--   middle of doing during typechecking.
type TCStack = [LocatedTCFrame]

------------------------------------------------------------
-- Type source

-- | The source of a type during typechecking.
data Source
  = -- | An expected type that was "pushed down" from the context.
    Expected
  | -- | An actual/inferred type that was "pulled up" from a term.
    Actual
  deriving (Int -> Source -> ShowS
[Source] -> ShowS
Source -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Source] -> ShowS
$cshowList :: [Source] -> ShowS
show :: Source -> String
$cshow :: Source -> String
showsPrec :: Int -> Source -> ShowS
$cshowsPrec :: Int -> Source -> ShowS
Show, Source -> Source -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Source -> Source -> Bool
$c/= :: Source -> Source -> Bool
== :: Source -> Source -> Bool
$c== :: Source -> Source -> Bool
Eq, Eq Source
Source -> Source -> Bool
Source -> Source -> Ordering
Source -> Source -> Source
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Source -> Source -> Source
$cmin :: Source -> Source -> Source
max :: Source -> Source -> Source
$cmax :: Source -> Source -> Source
>= :: Source -> Source -> Bool
$c>= :: Source -> Source -> Bool
> :: Source -> Source -> Bool
$c> :: Source -> Source -> Bool
<= :: Source -> Source -> Bool
$c<= :: Source -> Source -> Bool
< :: Source -> Source -> Bool
$c< :: Source -> Source -> Bool
compare :: Source -> Source -> Ordering
$ccompare :: Source -> Source -> Ordering
Ord, Source
forall a. a -> a -> Bounded a
maxBound :: Source
$cmaxBound :: Source
minBound :: Source
$cminBound :: Source
Bounded, Int -> Source
Source -> Int
Source -> [Source]
Source -> Source
Source -> Source -> [Source]
Source -> Source -> Source -> [Source]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Source -> Source -> Source -> [Source]
$cenumFromThenTo :: Source -> Source -> Source -> [Source]
enumFromTo :: Source -> Source -> [Source]
$cenumFromTo :: Source -> Source -> [Source]
enumFromThen :: Source -> Source -> [Source]
$cenumFromThen :: Source -> Source -> [Source]
enumFrom :: Source -> [Source]
$cenumFrom :: Source -> [Source]
fromEnum :: Source -> Int
$cfromEnum :: Source -> Int
toEnum :: Int -> Source
$ctoEnum :: Int -> Source
pred :: Source -> Source
$cpred :: Source -> Source
succ :: Source -> Source
$csucc :: Source -> Source
Enum)

-- | Generic eliminator for 'Source'.  Choose the first argument if
--   the 'Source' is 'Expected', and the second argument if 'Actual'.
withSource :: Source -> a -> a -> a
withSource :: forall a. Source -> a -> a -> a
withSource Source
Expected a
e a
_ = a
e
withSource Source
Actual a
_ a
a = a
a

-- | A value along with its source (expected vs actual).
type Sourced a = (Source, a)

-- | A "join" where an expected thing meets an actual thing.
newtype Join a = Join (Source -> a)

instance (Show a) => Show (Join a) where
  show :: Join a -> String
show (forall a. Join a -> (a, a)
getJoin -> (a
e, a
a)) = String
"(expected: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
e forall a. Semigroup a => a -> a -> a
<> String
", actual: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
a forall a. Semigroup a => a -> a -> a
<> String
")"

type TypeJoin = Join UType

-- | Create a 'Join' from an expected thing and an actual thing (in that order).
joined :: a -> a -> Join a
joined :: forall a. a -> a -> Join a
joined a
expect a
actual = forall a. (Source -> a) -> Join a
Join (\case Source
Expected -> a
expect; Source
Actual -> a
actual)

-- | Create a 'Join' from a 'Sourced' thing together with another
--   thing (which is assumed to have the opposite 'Source').
mkJoin :: Sourced a -> a -> Join a
mkJoin :: forall a. Sourced a -> a -> Join a
mkJoin (Source
src, a
a1) a
a2 = forall a. (Source -> a) -> Join a
Join forall a b. (a -> b) -> a -> b
$ \Source
s -> if Source
s forall a. Eq a => a -> a -> Bool
== Source
src then a
a1 else a
a2

-- | Convert a 'Join' into a pair of (expected, actual).
getJoin :: Join a -> (a, a)
getJoin :: forall a. Join a -> (a, a)
getJoin (Join Source -> a
j) = (Source -> a
j Source
Expected, Source -> a
j Source
Actual)

------------------------------------------------------------
-- Type checking monad

-- | The concrete monad used for type checking.  'IntBindingT' is a
--   monad transformer provided by the @unification-fd@ library which
--   supports various operations such as generating fresh variables
--   and unifying things.
--
--   Note that we are sort of constrained to use a concrete monad stack by
--   @unification-fd@, which has some strange types on some of its exported
--   functions that actually require various monad transformers to be stacked
--   in certain ways.  For example, see <https://hackage.haskell.org/package/unification-fd-0.11.2/docs/Control-Unification.html#v:unify>.  I don't really see a way
--   to use "capability style" like we do elsewhere in the codebase.
type TC = ReaderT UCtx (ReaderT TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))

-- | Push a frame on the typechecking stack within a local 'TC'
--   computation.
withFrame :: SrcLoc -> TCFrame -> TC a -> TC a
withFrame :: forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
f = forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT (forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (SrcLoc -> TCFrame -> LocatedTCFrame
LocatedTCFrame SrcLoc
l TCFrame
f forall a. a -> [a] -> [a]
:))

-- | Get the current typechecking stack.
getTCStack :: TC TCStack
getTCStack :: TC TCStack
getTCStack = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask

------------------------------------------------------------

-- | Run a top-level inference computation, returning either a
--   'TypeErr' or a fully resolved 'TModule'.
runTC :: TCtx -> TC UModule -> Either ContextualTypeErr TModule
runTC :: Ctx Polytype -> TC UModule -> Either ContextualTypeErr TModule
runTC Ctx Polytype
ctx =
  (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall u. HasBindings u => u -> TC u
applyBindings)
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ( forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \(Module Syntax' (UTerm TypeF IntVar)
u UCtx
uctx) ->
              forall s t. Syntax' s -> Ctx t -> Module s t
Module
                forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. Maybe a -> TC a
checkPredicative forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => U t -> Maybe t
fromU forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTerm TypeF IntVar -> TC UPolytype
generalize)) Syntax' (UTerm TypeF IntVar)
u
                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Maybe a -> TC a
checkPredicative (forall t. WithU t => U t -> Maybe t
fromU UCtx
uctx)
        )
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall t. WithU t => t -> U t
toU Ctx Polytype
ctx)
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT []
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT
    forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a. Identity a -> a
runIdentity

checkPredicative :: Maybe a -> TC a
checkPredicative :: forall a. Maybe a -> TC a
checkPredicative = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeErr -> ContextualTypeErr
mkRawTypeErr TypeErr
Impredicative)) forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Look up a variable in the ambient type context, either throwing
--   an 'UnboundVar' error if it is not found, or opening its
--   associated 'UPolytype' with fresh unification variables via
--   'instantiate'.
lookup :: SrcLoc -> Var -> TC UType
lookup :: SrcLoc -> Var -> TC (UTerm TypeF IntVar)
lookup SrcLoc
loc Var
x = do
  UCtx
ctx <- TC UCtx
getCtx
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
loc forall a b. (a -> b) -> a -> b
$ Var -> TypeErr
UnboundVar Var
x) UPolytype -> TC (UTerm TypeF IntVar)
instantiate (forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x UCtx
ctx)

-- | Get the current type context.
getCtx :: TC UCtx
getCtx :: TC UCtx
getCtx = forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Catch any thrown type errors and re-throw them with an added source
--   location.
addLocToTypeErr :: SrcLoc -> TC a -> TC a
addLocToTypeErr :: forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l TC a
m =
  TC a
m forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
    CTE SrcLoc
NoLoc TCStack
_ TypeErr
te -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l TypeErr
te
    ContextualTypeErr
te -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ContextualTypeErr
te

------------------------------------------------------------
-- Dealing with variables: free variables, fresh variables,
-- substitution

-- | @unification-fd@ does not provide an 'Ord' instance for 'IntVar',
--   so we must provide our own, in order to be able to store
--   'IntVar's in a 'Set'.
deriving instance Ord IntVar

-- | A class for getting the free unification variables of a thing.
class FreeVars a where
  freeVars :: a -> TC (Set IntVar)

-- | We can get the free unification variables of a 'UType'.
instance FreeVars UType where
  freeVars :: UTerm TypeF IntVar -> TC (Set IntVar)
freeVars UTerm TypeF IntVar
ut = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UTerm TypeF IntVar
ut

-- | We can also get the free variables of a polytype.
instance (FreeVars t) => FreeVars (Poly t) where
  freeVars :: Poly t -> TC (Set IntVar)
freeVars (Forall [Var]
_ t
t) = forall a. FreeVars a => a -> TC (Set IntVar)
freeVars t
t

-- | We can get the free variables in any polytype in a context.
instance FreeVars UCtx where
  freeVars :: UCtx -> TC (Set IntVar)
freeVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. FreeVars a => a -> TC (Set IntVar)
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Ctx t -> Map Var t
unCtx

-- | Generate a fresh unification variable.
fresh :: TC UType
fresh :: TC (UTerm TypeF IntVar)
fresh = forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar)

-- | Perform a substitution over a 'UType', substituting for both type
--   and unification variables.  Note that since 'UType's do not have
--   any binding constructs, we don't have to worry about ignoring
--   bound variables; all variables in a 'UType' are free.
substU :: Map (Either Var IntVar) UType -> UType -> UType
substU :: Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU Map (Either Var IntVar) (UTerm TypeF IntVar)
m =
  forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
    (\IntVar
v -> forall a. a -> Maybe a -> a
fromMaybe (forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. b -> Either a b
Right IntVar
v) Map (Either Var IntVar) (UTerm TypeF IntVar)
m))
    ( \case
        TyVarF Var
v -> forall a. a -> Maybe a -> a
fromMaybe (Var -> UTerm TypeF IntVar
UTyVar Var
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. a -> Either a b
Left Var
v) Map (Either Var IntVar) (UTerm TypeF IntVar)
m)
        TypeF (UTerm TypeF IntVar)
f -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeF (UTerm TypeF IntVar)
f
    )

-- | Make sure no skolem variables escape.
noSkolems :: SrcLoc -> UPolytype -> TC ()
noSkolems :: SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l (Forall [Var]
xs UTerm TypeF IntVar
upty) = do
  UTerm TypeF IntVar
upty' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
upty
  let tyvs :: Set Var
tyvs =
        forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
          (forall a b. a -> b -> a
const forall a. Set a
S.empty)
          (\case TyVarF Var
v -> forall a. a -> Set a
S.singleton Var
v; TypeF (Set Var)
f -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)
          UTerm TypeF IntVar
upty'
      ftyvs :: Set Var
ftyvs = Set Var
tyvs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> Maybe a
S.lookupMin Set Var
ftyvs) forall a b. (a -> b) -> a -> b
$ forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> TypeErr
EscapedSkolem

-- ~~~~ Note [lookupMin to get an arbitrary element]
--
-- `S.lookupMin :: Set a -> Maybe a` returns the smallest
-- element of a set, or Nothing if the set is empty. We don't
-- actually care about getting the *smallest* type variable, but
-- lookupMin is a convenient way to say "just get one element if
-- any exist". The forM_ is actually over the Maybe so it represents
-- doing the throwTypeErr either zero or one time, depending on
-- whether lookupMin returns Nothing or Just.

------------------------------------------------------------
-- Lifted stuff from unification-fd

infix 4 =:=

-- | @unify t expTy actTy@ ensures that the given two types are equal.
--   If we know the actual term @t@ which is supposed to have these
--   types, we can use it to generate better error messages.
--
--   We first do a quick-and-dirty check to see whether we know for
--   sure the types either are or cannot be equal, generating an
--   equality constraint for the unifier as a last resort.
unify :: Maybe Syntax -> TypeJoin -> TC UType
unify :: Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify Maybe Syntax
ms TypeJoin
j = case UTerm TypeF IntVar -> UTerm TypeF IntVar -> UnifyStatus
unifyCheck UTerm TypeF IntVar
expected UTerm TypeF IntVar
actual of
  UnifyStatus
Apart -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
NoLoc forall a b. (a -> b) -> a -> b
$ Maybe Syntax -> TypeJoin -> TypeErr
Mismatch Maybe Syntax
ms TypeJoin
j
  UnifyStatus
Equal -> forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
expected
  UnifyStatus
MightUnify -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
expected forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
U.=:= UTerm TypeF IntVar
actual
 where
  (UTerm TypeF IntVar
expected, UTerm TypeF IntVar
actual) = forall a. Join a -> (a, a)
getJoin TypeJoin
j

-- | Ensure two types are the same.
(=:=) :: UType -> UType -> TC UType
UTerm TypeF IntVar
ty1 =:= :: UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
ty2 = Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify forall a. Maybe a
Nothing (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2)

-- | @unification-fd@ provides a function 'U.applyBindings' which
--   fully substitutes for any bound unification variables (for
--   efficiency, it does not perform such substitution as it goes
--   along).  The 'HasBindings' class is for anything which has
--   unification variables in it and to which we can usefully apply
--   'U.applyBindings'.
class HasBindings u where
  applyBindings :: u -> TC u

instance HasBindings UType where
  applyBindings :: UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
applyBindings = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
U.applyBindings

instance HasBindings UPolytype where
  applyBindings :: UPolytype -> TC UPolytype
applyBindings (Forall [Var]
xs UTerm TypeF IntVar
u) = forall t. [Var] -> t -> Poly t
Forall [Var]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
u

instance HasBindings UCtx where
  applyBindings :: UCtx -> TC UCtx
applyBindings = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall u. HasBindings u => u -> TC u
applyBindings

instance (HasBindings u, Data u) => HasBindings (Term' u) where
  applyBindings :: Term' u -> TC (Term' u)
applyBindings = forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> a -> m a
gmapM (forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM (forall u. HasBindings u => u -> TC u
applyBindings @(Syntax' u)))

instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
  applyBindings :: Syntax' u -> TC (Syntax' u)
applyBindings (Syntax' SrcLoc
l Term' u
t u
u) = forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings Term' u
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> TC u
applyBindings u
u

instance HasBindings UModule where
  applyBindings :: UModule -> TC UModule
applyBindings (Module Syntax' (UTerm TypeF IntVar)
u UCtx
uctx) = forall s t. Syntax' s -> Ctx t -> Module s t
Module forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings Syntax' (UTerm TypeF IntVar)
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> TC u
applyBindings UCtx
uctx

------------------------------------------------------------
-- Converting between mono- and polytypes

-- | To 'instantiate' a 'UPolytype', we generate a fresh unification
--   variable for each variable bound by the `Forall`, and then
--   substitute them throughout the type.
instantiate :: UPolytype -> TC UType
instantiate :: UPolytype -> TC (UTerm TypeF IntVar)
instantiate (Forall [Var]
xs UTerm TypeF IntVar
uty) = do
  [UTerm TypeF IntVar]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const TC (UTerm TypeF IntVar)
fresh) [Var]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) [UTerm TypeF IntVar]
xs')) UTerm TypeF IntVar
uty

-- | 'skolemize' is like 'instantiate', except we substitute fresh
--   /type/ variables instead of unification variables.  Such
--   variables cannot unify with anything other than themselves.  This
--   is used when checking something with a polytype explicitly
--   specified by the user.
skolemize :: UPolytype -> TC UType
skolemize :: UPolytype -> TC (UTerm TypeF IntVar)
skolemize (Forall [Var]
xs UTerm TypeF IntVar
uty) = do
  [UTerm TypeF IntVar]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const TC (UTerm TypeF IntVar)
fresh) [Var]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) (forall a b. (a -> b) -> [a] -> [b]
map forall {t :: * -> *}.
Show (t (UTerm t IntVar)) =>
UTerm t IntVar -> UTerm TypeF IntVar
toSkolem [UTerm TypeF IntVar]
xs'))) UTerm TypeF IntVar
uty
 where
  toSkolem :: UTerm t IntVar -> UTerm TypeF IntVar
toSkolem (UVar IntVar
v) = Var -> UTerm TypeF IntVar
UTyVar (Var -> IntVar -> Var
mkVarName Var
"s" IntVar
v)
  toSkolem UTerm t IntVar
x = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Non-UVar in skolemize.toSkolem: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UTerm t IntVar
x

-- | 'generalize' is the opposite of 'instantiate': add a 'Forall'
--   which closes over all free type and unification variables.
--
--   Pick nice type variable names instead of reusing whatever fresh
--   names happened to be used for the free variables.
generalize :: UType -> TC UPolytype
generalize :: UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
uty = do
  UTerm TypeF IntVar
uty' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
uty
  UCtx
ctx <- TC UCtx
getCtx
  Set IntVar
tmfvs <- forall a. FreeVars a => a -> TC (Set IntVar)
freeVars UTerm TypeF IntVar
uty'
  Set IntVar
ctxfvs <- forall a. FreeVars a => a -> TC (Set IntVar)
freeVars UCtx
ctx
  let fvs :: [IntVar]
fvs = forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ Set IntVar
tmfvs forall a. Ord a => Set a -> Set a -> Set a
\\ Set IntVar
ctxfvs
      alphabet :: String
alphabet = [Char
'a' .. Char
'z']
      -- Infinite supply of pretty names a, b, ..., z, a0, ... z0, a1, ... z1, ...
      prettyNames :: [Var]
prettyNames = forall a b. (a -> b) -> [a] -> [b]
map String -> Var
T.pack (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
: []) String
alphabet forall a. [a] -> [a] -> [a]
++ [Char
x forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
n | Int
n <- [Int
0 :: Int ..], Char
x <- String
alphabet])
      -- Associate each free variable with a new pretty name
      renaming :: [(IntVar, Var)]
renaming = forall a b. [a] -> [b] -> [(a, b)]
zip [IntVar]
fvs [Var]
prettyNames
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    forall t. [Var] -> t -> Poly t
Forall
      (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(IntVar, Var)]
renaming)
      (Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. b -> Either a b
Right forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Var -> UTerm TypeF IntVar
UTyVar) forall a b. (a -> b) -> a -> b
$ [(IntVar, Var)]
renaming) UTerm TypeF IntVar
uty')

------------------------------------------------------------
-- Type errors

-- | A type error along with various contextual information to help us
--   generate better error messages.
data ContextualTypeErr = CTE {ContextualTypeErr -> SrcLoc
cteSrcLoc :: SrcLoc, ContextualTypeErr -> TCStack
cteStack :: TCStack, ContextualTypeErr -> TypeErr
cteTypeErr :: TypeErr}
  deriving (Int -> ContextualTypeErr -> ShowS
[ContextualTypeErr] -> ShowS
ContextualTypeErr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ContextualTypeErr] -> ShowS
$cshowList :: [ContextualTypeErr] -> ShowS
show :: ContextualTypeErr -> String
$cshow :: ContextualTypeErr -> String
showsPrec :: Int -> ContextualTypeErr -> ShowS
$cshowsPrec :: Int -> ContextualTypeErr -> ShowS
Show)

-- | Create a raw 'ContextualTypeErr' with no context information.
mkRawTypeErr :: TypeErr -> ContextualTypeErr
mkRawTypeErr :: TypeErr -> ContextualTypeErr
mkRawTypeErr = SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
CTE SrcLoc
NoLoc []

-- | Create a 'ContextualTypeErr' value from a 'TypeErr' and context.
mkTypeErr :: SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr :: SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr = SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
CTE

-- | Throw a 'ContextualTypeErr'.
throwTypeErr :: SrcLoc -> TypeErr -> TC a
throwTypeErr :: forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l TypeErr
te = do
  TCStack
stk <- TC TCStack
getTCStack
  forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr SrcLoc
l TCStack
stk TypeErr
te

-- | Errors that can occur during type checking.  The idea is that
--   each error carries information that can be used to help explain
--   what went wrong (though the amount of information carried can and
--   should be very much improved in the future); errors can then
--   separately be pretty-printed to display them to the user.
data TypeErr
  = -- | An undefined variable was encountered.
    UnboundVar Var
  | -- | A Skolem variable escaped its local context.
    EscapedSkolem Var
  | -- | Occurs check failure, i.e. infinite type.
    Infinite IntVar UType
  | -- | Error generated by the unifier.
    UnifyErr (TypeF UType) (TypeF UType)
  | -- | Type mismatch caught by 'unifyCheck'.  The given term was
    --   expected to have a certain type, but has a different type
    --   instead.
    Mismatch (Maybe Syntax) TypeJoin
  | -- | Lambda argument type mismatch.
    LambdaArgMismatch TypeJoin
  | -- | Record field mismatch, i.e. based on the expected type we
    --   were expecting a record with certain fields, but found one with
    --   a different field set.
    FieldsMismatch (Join (Set Var))
  | -- | A definition was encountered not at the top level.
    DefNotTopLevel Term
  | -- | A term was encountered which we cannot infer the type of.
    --   This should never happen.
    CantInfer Term
  | -- | We can't infer the type of a record projection @r.x@ if we
    --   don't concretely know the type of the record @r@.
    CantInferProj Term
  | -- | An attempt to project out a nonexistent field
    UnknownProj Var Term
  | -- | An invalid argument was provided to @atomic@.
    InvalidAtomic InvalidAtomicReason Term
  | -- | Some unification variables ended up in a type, probably due to
    --   impredicativity.  See https://github.com/swarm-game/swarm/issues/351 .
    Impredicative
  deriving (Int -> TypeErr -> ShowS
[TypeErr] -> ShowS
TypeErr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeErr] -> ShowS
$cshowList :: [TypeErr] -> ShowS
show :: TypeErr -> String
$cshow :: TypeErr -> String
showsPrec :: Int -> TypeErr -> ShowS
$cshowsPrec :: Int -> TypeErr -> ShowS
Show)

-- | Various reasons the body of an @atomic@ might be invalid.
data InvalidAtomicReason
  = -- | The argument has too many tangible commands.
    TooManyTicks Int
  | -- | The argument uses some way to duplicate code: @def@, @let@, or lambda.
    AtomicDupingThing
  | -- | The argument referred to a variable with a non-simple type.
    NonSimpleVarType Var UPolytype
  | -- | The argument had a nested @atomic@
    NestedAtomic
  | -- | The argument contained a long command
    LongConst
  deriving (Int -> InvalidAtomicReason -> ShowS
[InvalidAtomicReason] -> ShowS
InvalidAtomicReason -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InvalidAtomicReason] -> ShowS
$cshowList :: [InvalidAtomicReason] -> ShowS
show :: InvalidAtomicReason -> String
$cshow :: InvalidAtomicReason -> String
showsPrec :: Int -> InvalidAtomicReason -> ShowS
$cshowsPrec :: Int -> InvalidAtomicReason -> ShowS
Show)

instance Fallible TypeF IntVar ContextualTypeErr where
  occursFailure :: IntVar -> UTerm TypeF IntVar -> ContextualTypeErr
occursFailure IntVar
v UTerm TypeF IntVar
t = TypeErr -> ContextualTypeErr
mkRawTypeErr (IntVar -> UTerm TypeF IntVar -> TypeErr
Infinite IntVar
v UTerm TypeF IntVar
t)
  mismatchFailure :: TypeF (UTerm TypeF IntVar)
-> TypeF (UTerm TypeF IntVar) -> ContextualTypeErr
mismatchFailure TypeF (UTerm TypeF IntVar)
t1 TypeF (UTerm TypeF IntVar)
t2 = TypeErr -> ContextualTypeErr
mkRawTypeErr (TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> TypeErr
UnifyErr TypeF (UTerm TypeF IntVar)
t1 TypeF (UTerm TypeF IntVar)
t2)

------------------------------------------------------------
-- Type decomposition

-- | Decompose a type that is supposed to be a delay type.  Also take
--   the term which is supposed to have that type, for use in error
--   messages.
decomposeDelayTy :: Syntax -> Sourced UType -> TC UType
decomposeDelayTy :: Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeDelayTy Syntax
_ (Source
_, UTyDelay UTerm TypeF IntVar
a) = forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeDelayTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
  UTerm TypeF IntVar
a <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyDelay UTerm TypeF IntVar
a))
  forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a

-- | Decompose a type that is supposed to be a command type. Also take
--   the term which is supposed to have that type, for use in error
--   messages.
decomposeCmdTy :: Syntax -> Sourced UType -> TC UType
decomposeCmdTy :: Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
_ (Source
_, UTyCmd UTerm TypeF IntVar
a) = forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeCmdTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
  UTerm TypeF IntVar
a <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
a))
  forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a

-- | Decompose a type that is supposed to be a function type. Also take
--   the term which is supposed to have that type, for use in error
--   messages.
decomposeFunTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeFunTy :: Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
_ (Source
_, UTyFun UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2) = forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
decomposeFunTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
  UTerm TypeF IntVar
ty1 <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
ty2 <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2))
  forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)

-- | Decompose a type that is supposed to be a product type. Also take
--   the term which is supposed to have that type, for use in error
--   messages.
decomposeProdTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeProdTy :: Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeProdTy Syntax
_ (Source
_, UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2) = forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
decomposeProdTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
  UTerm TypeF IntVar
ty1 <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
ty2 <- TC (UTerm TypeF IntVar)
fresh
  UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2))
  forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)

------------------------------------------------------------
-- Type inference / checking

-- | Top-level type inference function: given a context of definition
--   types and a top-level term, either return a type error or its
--   type as a 'TModule'.
inferTop :: TCtx -> Syntax -> Either ContextualTypeErr TModule
inferTop :: Ctx Polytype -> Syntax -> Either ContextualTypeErr TModule
inferTop Ctx Polytype
ctx = Ctx Polytype -> TC UModule -> Either ContextualTypeErr TModule
runTC Ctx Polytype
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. Syntax -> TC UModule
inferModule

-- | Infer the signature of a top-level expression which might
--   contain definitions.
inferModule :: Syntax -> TC UModule
inferModule :: Syntax -> TC UModule
inferModule s :: Syntax
s@(Syntax SrcLoc
l Term
t) = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
  -- For definitions with no type signature, make up a fresh type
  -- variable for the body, infer the body under an extended context,
  -- and unify the two.  Then generalize the type and return an
  -- appropriate context.
  SDef Bool
r LocVar
x Maybe Polytype
Nothing Syntax
t1 -> forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l (Var -> TCFrame
TCDef (LocVar -> Var
lvVar LocVar
x)) forall a b. (a -> b) -> a -> b
$ do
    UTerm TypeF IntVar
xTy <- TC (UTerm TypeF IntVar)
fresh
    Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
    UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t1) (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
xTy (Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
    UPolytype
pty <- UTerm TypeF IntVar -> TC UPolytype
generalize (Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x forall a. Maybe a
Nothing Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
pty)

  -- If a (poly)type signature has been provided, skolemize it and
  -- check the definition.
  SDef Bool
r LocVar
x (Just Polytype
pty) Syntax
t1 -> forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l (Var -> TCFrame
TCDef (LocVar -> Var
lvVar LocVar
x)) forall a b. (a -> b) -> a -> b
$ do
    let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
    UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
    Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
t1 UTerm TypeF IntVar
uty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x (forall a. a -> Maybe a
Just Polytype
pty) Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
upty)

  -- To handle a 'TBind', infer the types of both sides, combining the
  -- returned modules appropriately.  Have to be careful to use the
  -- correct context when checking the right-hand side in particular.
  SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
    -- First, infer the left side.
    Module Syntax' (UTerm TypeF IntVar)
c1' UCtx
ctx1 <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindL forall a b. (a -> b) -> a -> b
$ Syntax -> TC UModule
inferModule Syntax
c1
    UTerm TypeF IntVar
a <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c1 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)

    -- Note we generalize here, similar to how we generalize at let
    -- bindings, since the result type of the LHS will be the type of
    -- the variable (if there is one).  In many cases this doesn't
    -- matter, but variables bound by top-level bind expressions can
    -- end up in the top-level context (e.g. if someone writes `x <-
    -- blah` at the REPL). We must generalize here, before adding the
    -- variable to the context, since afterwards it will be too late:
    -- we cannot generalize over any unification variables occurring
    -- in the context.
    --
    -- This is safe since it is always safe to generalize at any point.
    --
    -- See #351, #1501.
    UPolytype
genA <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
a

    -- Now infer the right side under an extended context: things in
    -- scope on the right-hand side include both any definitions
    -- created by the left-hand side, as well as a variable as in @x
    -- <- c1; c2@.  The order of extensions here matters: in theory,
    -- c1 could define something with the same name as x, in which
    -- case the bound x should shadow the defined one; hence, we apply
    -- that binding /after/ (i.e. /within/) the application of @ctx1@.
    forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Ctx t -> m a -> m a
withBindings UCtx
ctx1 forall a b. (a -> b) -> a -> b
$
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx forall a b. (a -> b) -> a -> b
$ do
        Module Syntax' (UTerm TypeF IntVar)
c2' UCtx
ctx2 <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindR forall a b. (a -> b) -> a -> b
$ Syntax -> TC UModule
inferModule Syntax
c2

        -- We don't actually need the result type since we're just
        -- going to return the entire type, but it's important to
        -- ensure it's a command type anyway.  Otherwise something
        -- like 'move; 3' would be accepted with type int.
        UTerm TypeF IntVar
_ <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c2 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)

        -- Ctx.union is right-biased, so ctx1 `union` ctx2 means later
        -- definitions will shadow previous ones.  Include the binder
        -- (if any) as well, since binders are made available at the top
        -- level, just like definitions. e.g. if the user writes `r <- build {move}`,
        -- then they will be able to refer to r again later.
        let ctxX :: UCtx
ctxX = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall t. Ctx t
Ctx.empty ((forall t. Var -> t -> Ctx t
`Ctx.singleton` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          forall s t. Syntax' s -> Ctx t -> Module s t
Module
            (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' (UTerm TypeF IntVar)
c1' Syntax' (UTerm TypeF IntVar)
c2') (Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
            (UCtx
ctx1 forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctxX forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctx2)

  -- In all other cases, there can no longer be any definitions in the
  -- term, so delegate to 'infer'.
  Term
_anyOtherTerm -> forall s t. Syntax' s -> Module s t
trivMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
s

-- | Infer the type of a term which does not contain definitions,
--   returning a type-annotated term.
--
--   The only cases explicitly handled in 'infer' are those where
--   pushing an expected type down into the term can't possibly help,
--   e.g. most primitives, function application, and binds.
--
--   For most everything else we prefer 'check' because it can often
--   result in better and more localized type error messages.
infer :: Syntax -> TC (Syntax' UType)
infer :: Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer s :: Syntax
s@(Syntax SrcLoc
l Term
t) = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
  -- Primitives, i.e. things for which we immediately know the only
  -- possible correct type, and knowing an expected type would provide
  -- no extra information.
  Term
TUnit -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall ty. Term' ty
TUnit UTerm TypeF IntVar
UTyUnit
  TConst Const
c -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UPolytype -> TC (UTerm TypeF IntVar)
instantiate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. WithU t => t -> U t
toU forall a b. (a -> b) -> a -> b
$ Const -> Polytype
inferConst Const
c)
  TDir Direction
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Direction -> Term' ty
TDir Direction
d) UTerm TypeF IntVar
UTyDir
  TInt Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Integer -> Term' ty
TInt Integer
n) UTerm TypeF IntVar
UTyInt
  TAntiInt Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiInt Var
x) UTerm TypeF IntVar
UTyInt
  TText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TText Var
x) UTerm TypeF IntVar
UTyText
  TAntiText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiText Var
x) UTerm TypeF IntVar
UTyText
  TBool Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Bool -> Term' ty
TBool Bool
b) UTerm TypeF IntVar
UTyBool
  TRobot Int
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Term' ty
TRobot Int
r) UTerm TypeF IntVar
UTyActor
  TRequireDevice Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TRequireDevice Var
d) (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)
  TRequire Int
n Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Var -> Term' ty
TRequire Int
n Var
d) (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)
  SRequirements Var
x Syntax
t1 -> do
    Syntax' (UTerm TypeF IntVar)
t1' <- Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Syntax' ty -> Term' ty
SRequirements Var
x Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)

  -- We should never encounter a TRef since they do not show up in
  -- surface syntax, only as values while evaluating (*after*
  -- typechecking).
  TRef Int
_ -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInfer Term
t
  -- Just look up variables in the context.
  TVar Var
x -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TVar Var
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> Var -> TC (UTerm TypeF IntVar)
lookup SrcLoc
l Var
x
  -- It is helpful to handle lambdas in inference mode as well as
  -- checking mode; in particular, we can handle lambdas with an
  -- explicit type annotation on the argument.  Just infer the body
  -- under an extended context and return the appropriate function
  -- type.
  SLam LocVar
x (Just Type
argTy) Syntax
body -> do
    let uargTy :: U Type
uargTy = forall t. WithU t => t -> U t
toU Type
argTy
    Syntax' (UTerm TypeF IntVar)
body' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
uargTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
body
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x (forall a. a -> Maybe a
Just Type
argTy) Syntax' (UTerm TypeF IntVar)
body') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
uargTy (Syntax' (UTerm TypeF IntVar)
body' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))

  -- Need special case here for applying 'atomic' or 'instant' so we
  -- don't handle it with the case for generic type application.
  -- This must come BEFORE the SApp case.
  TConst Const
c :$: Syntax
_
    | Const
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> TC (UTerm TypeF IntVar)
fresh forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
s
  -- It works better to handle applications in *inference* mode.
  -- Knowing the expected result type of an application does not
  -- really help much.  In the typical case, the function being
  -- applied is either (1) a primitive or variable whose type we can
  -- easily infer, or (2) a nested application; in the second case in
  -- particular, handling applications in inference mode means we can
  -- stay in inference mode the whole way down the left-hand side of
  -- the chain of applications.  If we handled applications in
  -- checking mode, we would constantly flip back and forth between
  -- inference & checking and generate a fresh unification variable
  -- each time.
  SApp Syntax
f Syntax
x -> do
    -- Infer the type of the left-hand side and make sure it has a function type.
    Syntax' (UTerm TypeF IntVar)
f' <- Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
f
    (UTerm TypeF IntVar
argTy, UTerm TypeF IntVar
resTy) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
f (Source
Actual, Syntax' (UTerm TypeF IntVar)
f' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)

    -- Then check that the argument has the right type.
    Syntax' (UTerm TypeF IntVar)
x' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
x UTerm TypeF IntVar
argTy

    -- Call applyBindings explicitly, so that anything we learned
    -- about unification variables while checking the type of the
    -- argument can flow to later steps.  This is especially helpful
    -- while checking applications of polymorphic multi-argument
    -- functions such as 'if'.  Without this call to 'applyBindings',
    -- type mismatches between the branches of an 'if' tend to get
    -- caught in the unifier, resulting in vague "can't unify"
    -- messages (for example, "if true {3} {move}" yields "can't
    -- unify int and cmd unit").  With this 'applyBindings' call, we
    -- get more specific errors about how the second branch was
    -- expected to have the same type as the first (e.g. "expected
    -- `move` to have type `int`, but it actually has type `cmd
    -- unit`).
    UTerm TypeF IntVar
resTy' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
resTy

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' (UTerm TypeF IntVar)
f' Syntax' (UTerm TypeF IntVar)
x') UTerm TypeF IntVar
resTy'

  -- We handle binds in inference mode for a similar reason to
  -- application.
  SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
    Syntax' (UTerm TypeF IntVar)
c1' <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindL forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
c1
    UTerm TypeF IntVar
a <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c1 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
    UPolytype
genA <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
a
    Syntax' (UTerm TypeF IntVar)
c2' <-
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindR
        forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
c2
    UTerm TypeF IntVar
_ <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c2 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' (UTerm TypeF IntVar)
c1' Syntax' (UTerm TypeF IntVar)
c2') (Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)

  -- Handle record projection in inference mode.  Knowing the expected
  -- type of r.x doesn't really help since we must infer the type of r
  -- first anyway.
  SProj Syntax
t1 Var
x -> do
    Syntax' (UTerm TypeF IntVar)
t1' <- Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
    case Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType of
      UTyRcd Map Var (UTerm TypeF IntVar)
m -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var (UTerm TypeF IntVar)
m of
        Just UTerm TypeF IntVar
xTy -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax' (UTerm TypeF IntVar)
t1' Var
x) UTerm TypeF IntVar
xTy
        Maybe (UTerm TypeF IntVar)
Nothing -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Var -> Term -> TypeErr
UnknownProj Var
x (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax
t1 Var
x)
      UTerm TypeF IntVar
_ -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInferProj (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax
t1 Var
x)

  -- See Note [Checking and inference for record literals]
  SRcd Map Var (Maybe Syntax)
m -> do
    Map Var (Syntax' (UTerm TypeF IntVar))
m' <- forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
itraverse (\Var
x -> Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x))) Map Var (Maybe Syntax)
m
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var (Syntax' (UTerm TypeF IntVar))
m')) (Map Var (UTerm TypeF IntVar) -> UTerm TypeF IntVar
UTyRcd (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) Map Var (Syntax' (UTerm TypeF IntVar))
m'))

  -- To infer a type-annotated term, switch into checking mode.
  -- However, we must be careful to deal properly with polymorphic
  -- type annotations.
  SAnnotate Syntax
c Polytype
pty -> do
    let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
    -- Typecheck against skolemized polytype.
    UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
    Syntax' (UTerm TypeF IntVar)
_ <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
c UTerm TypeF IntVar
uty
    -- Make sure no skolem variables have escaped.
    TC UCtx
getCtx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l)
    -- If check against skolemized polytype is successful,
    -- instantiate polytype with unification variables.
    -- Free variables should be able to unify with anything in
    -- following typechecking steps.
    UTerm TypeF IntVar
iuty <- UPolytype -> TC (UTerm TypeF IntVar)
instantiate UPolytype
upty
    Syntax' (UTerm TypeF IntVar)
c' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
c UTerm TypeF IntVar
iuty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Polytype -> Term' ty
SAnnotate Syntax' (UTerm TypeF IntVar)
c' Polytype
pty) (Syntax' (UTerm TypeF IntVar)
c' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)

  -- Fallback: to infer the type of anything else, make up a fresh unification
  -- variable for its type and check against it.
  Term
_ -> do
    UTerm TypeF IntVar
sTy <- TC (UTerm TypeF IntVar)
fresh
    Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
s UTerm TypeF IntVar
sTy

-- | Infer the type of a constant.
inferConst :: Const -> Polytype
inferConst :: Const -> Polytype
inferConst Const
c = case Const
c of
  Const
Wait -> [tyQ| int -> cmd unit |]
  Const
Noop -> [tyQ| cmd unit |]
  Const
Selfdestruct -> [tyQ| cmd unit |]
  Const
Move -> [tyQ| cmd unit |]
  Const
Backup -> [tyQ| cmd unit |]
  Const
Path -> [tyQ| (unit + int) -> ((int * int) + text) -> cmd (unit + dir) |]
  Const
Push -> [tyQ| cmd unit |]
  Const
Stride -> [tyQ| int -> cmd unit |]
  Const
Turn -> [tyQ| dir -> cmd unit |]
  Const
Grab -> [tyQ| cmd text |]
  Const
Harvest -> [tyQ| cmd text |]
  Const
Ignite -> [tyQ| dir -> cmd unit |]
  Const
Place -> [tyQ| text -> cmd unit |]
  Const
Ping -> [tyQ| actor -> cmd (unit + (int * int)) |]
  Const
Give -> [tyQ| actor -> text -> cmd unit |]
  Const
Equip -> [tyQ| text -> cmd unit |]
  Const
Unequip -> [tyQ| text -> cmd unit |]
  Const
Make -> [tyQ| text -> cmd unit |]
  Const
Has -> [tyQ| text -> cmd bool |]
  Const
Equipped -> [tyQ| text -> cmd bool |]
  Const
Count -> [tyQ| text -> cmd int |]
  Const
Reprogram -> [tyQ| actor -> {cmd a} -> cmd unit |]
  Const
Build -> [tyQ| {cmd a} -> cmd actor |]
  Const
Drill -> [tyQ| dir -> cmd (unit + text) |]
  Const
Use -> [tyQ| text -> dir -> cmd (unit + text) |]
  Const
Salvage -> [tyQ| cmd unit |]
  Const
Say -> [tyQ| text -> cmd unit |]
  Const
Listen -> [tyQ| cmd text |]
  Const
Log -> [tyQ| text -> cmd unit |]
  Const
View -> [tyQ| actor -> cmd unit |]
  Const
Appear -> [tyQ| text -> cmd unit |]
  Const
Create -> [tyQ| text -> cmd unit |]
  Const
Halt -> [tyQ| actor -> cmd unit |]
  Const
Time -> [tyQ| cmd int |]
  Const
Scout -> [tyQ| dir -> cmd bool |]
  Const
Whereami -> [tyQ| cmd (int * int) |]
  Const
Waypoint -> [tyQ| text -> int -> cmd (int * (int * int)) |]
  Const
Detect -> [tyQ| text -> ((int * int) * (int * int)) -> cmd (unit + (int * int)) |]
  Const
Resonate -> [tyQ| text -> ((int * int) * (int * int)) -> cmd int |]
  Const
Density -> [tyQ| ((int * int) * (int * int)) -> cmd int |]
  Const
Sniff -> [tyQ| text -> cmd int |]
  Const
Chirp -> [tyQ| text -> cmd dir |]
  Const
Watch -> [tyQ| dir -> cmd unit |]
  Const
Surveil -> [tyQ| (int * int) -> cmd unit |]
  Const
Heading -> [tyQ| cmd dir |]
  Const
Blocked -> [tyQ| cmd bool |]
  Const
Scan -> [tyQ| dir -> cmd (unit + text) |]
  Const
Upload -> [tyQ| actor -> cmd unit |]
  Const
Ishere -> [tyQ| text -> cmd bool |]
  Const
Isempty -> [tyQ| cmd bool |]
  Const
Self -> [tyQ| actor |]
  Const
Parent -> [tyQ| actor |]
  Const
Base -> [tyQ| actor |]
  Const
Meet -> [tyQ| cmd (unit + actor) |]
  Const
MeetAll -> [tyQ| (b -> actor -> cmd b) -> b -> cmd b |]
  Const
Whoami -> [tyQ| cmd text |]
  Const
Setname -> [tyQ| text -> cmd unit |]
  Const
Random -> [tyQ| int -> cmd int |]
  Const
Run -> [tyQ| text -> cmd unit |]
  Const
If -> [tyQ| bool -> {a} -> {a} -> a |]
  Const
Inl -> [tyQ| a -> a + b |]
  Const
Inr -> [tyQ| b -> a + b |]
  Const
Case -> [tyQ|a + b -> (a -> c) -> (b -> c) -> c |]
  Const
Fst -> [tyQ| a * b -> a |]
  Const
Snd -> [tyQ| a * b -> b |]
  Const
Force -> [tyQ| {a} -> a |]
  Const
Return -> [tyQ| a -> cmd a |]
  Const
Try -> [tyQ| {cmd a} -> {cmd a} -> cmd a |]
  Const
Undefined -> [tyQ| a |]
  Const
Fail -> [tyQ| text -> a |]
  Const
Not -> [tyQ| bool -> bool |]
  Const
Neg -> [tyQ| int -> int |]
  Const
Eq -> Polytype
cmpBinT
  Const
Neq -> Polytype
cmpBinT
  Const
Lt -> Polytype
cmpBinT
  Const
Gt -> Polytype
cmpBinT
  Const
Leq -> Polytype
cmpBinT
  Const
Geq -> Polytype
cmpBinT
  Const
And -> [tyQ| bool -> bool -> bool|]
  Const
Or -> [tyQ| bool -> bool -> bool|]
  Const
Add -> Polytype
arithBinT
  Const
Sub -> Polytype
arithBinT
  Const
Mul -> Polytype
arithBinT
  Const
Div -> Polytype
arithBinT
  Const
Exp -> Polytype
arithBinT
  Const
Format -> [tyQ| a -> text |]
  Const
Concat -> [tyQ| text -> text -> text |]
  Const
Chars -> [tyQ| text -> int |]
  Const
Split -> [tyQ| int -> text -> (text * text) |]
  Const
CharAt -> [tyQ| int -> text -> int |]
  Const
ToChar -> [tyQ| int -> text |]
  Const
AppF -> [tyQ| (a -> b) -> a -> b |]
  Const
Swap -> [tyQ| text -> cmd text |]
  Const
Atomic -> [tyQ| cmd a -> cmd a |]
  Const
Instant -> [tyQ| cmd a -> cmd a |]
  Const
Key -> [tyQ| text -> key |]
  Const
InstallKeyHandler -> [tyQ| text -> (key -> cmd unit) -> cmd unit |]
  Const
Teleport -> [tyQ| actor -> (int * int) -> cmd unit |]
  Const
As -> [tyQ| actor -> {cmd a} -> cmd a |]
  Const
RobotNamed -> [tyQ| text -> cmd actor |]
  Const
RobotNumbered -> [tyQ| int -> cmd actor |]
  Const
Knows -> [tyQ| text -> cmd bool |]
 where
  cmpBinT :: Polytype
cmpBinT = [tyQ| a -> a -> bool |]
  arithBinT :: Polytype
arithBinT = [tyQ| int -> int -> int |]

-- | @check t ty@ checks that @t@ has type @ty@, returning a
--   type-annotated AST if so.
--
--   We try to stay in checking mode as far as possible, decomposing
--   the expected type as we go and pushing it through the recursion.
check :: Syntax -> UType -> TC (Syntax' UType)
check :: Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check s :: Syntax
s@(Syntax SrcLoc
l Term
t) UTerm TypeF IntVar
expected = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
  -- if t : ty, then  {t} : {ty}.
  -- Note that in theory, if the @Maybe Var@ component of the @SDelay@
  -- is @Just@, we should typecheck the body under a context extended
  -- with a type binding for the variable, and ensure that the type of
  -- the variable is the same as the type inferred for the overall
  -- @SDelay@.  However, we rely on the invariant that such recursive
  -- @SDelay@ nodes are never generated from the surface syntax, only
  -- dynamically at runtime when evaluating recursive let or def expressions,
  -- so we don't have to worry about typechecking them here.
  SDelay DelayType
d Syntax
s1 -> do
    UTerm TypeF IntVar
ty1 <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeDelayTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
    Syntax' (UTerm TypeF IntVar)
s1' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
s1 UTerm TypeF IntVar
ty1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. DelayType -> Syntax' ty -> Term' ty
SDelay DelayType
d Syntax' (UTerm TypeF IntVar)
s1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyDelay UTerm TypeF IntVar
ty1)

  -- To check the type of a pair, make sure the expected type is a
  -- product type, and push the two types down into the left and right.
  SPair Syntax
s1 Syntax
s2 -> do
    (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeProdTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
    Syntax' (UTerm TypeF IntVar)
s1' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
s1 UTerm TypeF IntVar
ty1
    Syntax' (UTerm TypeF IntVar)
s2' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
s2 UTerm TypeF IntVar
ty2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SPair Syntax' (UTerm TypeF IntVar)
s1' Syntax' (UTerm TypeF IntVar)
s2') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2)

  -- To check a lambda, make sure the expected type is a function type.
  SLam LocVar
x Maybe Type
mxTy Syntax
body -> do
    (UTerm TypeF IntVar
argTy, UTerm TypeF IntVar
resTy) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
    case forall t. WithU t => t -> U t
toU Maybe Type
mxTy of
      Just UTerm TypeF IntVar
xTy -> case UTerm TypeF IntVar -> UTerm TypeF IntVar -> UnifyStatus
unifyCheck UTerm TypeF IntVar
argTy UTerm TypeF IntVar
xTy of
        -- Generate a special error when the explicit type annotation
        -- on a lambda doesn't match the expected type,
        -- e.g. (\x:int. x + 2) : text -> int, since the usual
        -- "expected/but got" language would probably be confusing.
        UnifyStatus
Apart -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ TypeJoin -> TypeErr
LambdaArgMismatch (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
argTy UTerm TypeF IntVar
xTy)
        -- Otherwise, make sure to unify the annotation with the
        -- expected argument type.
        UnifyStatus
_ -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
argTy UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
xTy
      Maybe (UTerm TypeF IntVar)
U (Maybe Type)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Syntax' (UTerm TypeF IntVar)
body' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
argTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
body UTerm TypeF IntVar
resTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x Maybe Type
mxTy Syntax' (UTerm TypeF IntVar)
body') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
argTy UTerm TypeF IntVar
resTy)

  -- Special case for checking the argument to 'atomic' (or
  -- 'instant').  'atomic t' has the same type as 't', which must have
  -- a type of the form 'cmd a' for some 'a'.

  TConst Const
c :$: Syntax
at
    | Const
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> do
        UTerm TypeF IntVar
argTy <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
        Syntax' (UTerm TypeF IntVar)
at' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
at (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
argTy)
        Syntax' (UTerm TypeF IntVar)
atomic' <- Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer (SrcLoc -> Term -> Syntax
Syntax SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
c))
        -- It's important that we typecheck the subterm @at@ *before* we
        -- check that it is a valid argument to @atomic@: this way we can
        -- ensure that we have already inferred the types of any variables
        -- referenced.
        --
        -- When c is Atomic we validate that the argument to atomic is
        -- guaranteed to operate within a single tick.  When c is Instant
        -- we skip this check.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Const
c forall a. Eq a => a -> a -> Bool
== Const
Atomic) forall a b. (a -> b) -> a -> b
$ Syntax -> TC ()
validAtomic Syntax
at
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' (UTerm TypeF IntVar)
atomic' Syntax' (UTerm TypeF IntVar)
at') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
argTy)
  -- Checking the type of a let-expression.
  SLet Bool
r LocVar
x Maybe Polytype
mxTy Syntax
t1 Syntax
t2 -> do
    (UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1') <- case Maybe Polytype
mxTy of
      -- No type annotation was provided for the let binding, so infer its type.
      Maybe Polytype
Nothing -> do
        -- The let could be recursive, so we must generate a fresh
        -- unification variable for the type of x and infer the type
        -- of t1 with x in the context.
        UTerm TypeF IntVar
xTy <- TC (UTerm TypeF IntVar)
fresh
        Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
        let uty :: UTerm TypeF IntVar
uty = Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType
        UTerm TypeF IntVar
_ <- UTerm TypeF IntVar
xTy UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
uty
        UPolytype
upty <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
uty
        forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1')
      -- An explicit polytype annotation has been provided. Skolemize it and check
      -- definition and body under an extended context.
      Just Polytype
pty -> do
        let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
        UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
        Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
t1 UTerm TypeF IntVar
uty
        forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1')

    -- Now check the type of the body.
    Syntax' (UTerm TypeF IntVar)
t2' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check Syntax
t2 UTerm TypeF IntVar
expected

    -- Make sure no skolem variables have escaped.
    TC UCtx
getCtx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l)

    -- Return the annotated let.
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool
-> LocVar -> Maybe Polytype -> Syntax' ty -> Syntax' ty -> Term' ty
SLet Bool
r LocVar
x Maybe Polytype
mxTy Syntax' (UTerm TypeF IntVar)
t1' Syntax' (UTerm TypeF IntVar)
t2') UTerm TypeF IntVar
expected

  -- Definitions can only occur at the top level.
  SDef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
DefNotTopLevel Term
t
  -- To check a record, ensure the expected type is a record type,
  -- ensure all the right fields are present, and push the expected
  -- types of all the fields down into recursive checks.
  --
  -- We have to be careful here --- if the expected type is not
  -- manifestly a record type but might unify with one (i.e. if the
  -- expected type is a variable) then we can't generate type
  -- variables for its subparts and push them, we have to switch
  -- completely into inference mode.  See Note [Checking and inference
  -- for record literals].
  SRcd Map Var (Maybe Syntax)
fields
    | UTyRcd Map Var (UTerm TypeF IntVar)
tyMap <- UTerm TypeF IntVar
expected -> do
        let expectedFields :: Set Var
expectedFields = forall k a. Map k a -> Set k
M.keysSet Map Var (UTerm TypeF IntVar)
tyMap
            actualFields :: Set Var
actualFields = forall k a. Map k a -> Set k
M.keysSet Map Var (Maybe Syntax)
fields
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set Var
actualFields forall a. Eq a => a -> a -> Bool
/= Set Var
expectedFields) forall a b. (a -> b) -> a -> b
$
          forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$
            Join (Set Var) -> TypeErr
FieldsMismatch (forall a. a -> a -> Join a
joined Set Var
expectedFields Set Var
actualFields)
        Map Var (Syntax' (UTerm TypeF IntVar))
m' <- forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
itraverse (\Var
x Maybe Syntax
ms -> Syntax
-> UTerm TypeF IntVar
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
check (forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x)) Maybe Syntax
ms) (Map Var (UTerm TypeF IntVar)
tyMap forall k a. Ord k => Map k a -> k -> a
! Var
x)) Map Var (Maybe Syntax)
fields
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var (Syntax' (UTerm TypeF IntVar))
m')) UTerm TypeF IntVar
expected

  -- Fallback: switch into inference mode, and check that the type we
  -- get is what we expected.
  Term
_ -> do
    Syntax' SrcLoc
l' Term' (UTerm TypeF IntVar)
t' UTerm TypeF IntVar
actual <- Syntax
-> ReaderT
     UCtx
     (ReaderT
        TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
     (Syntax' (UTerm TypeF IntVar))
infer Syntax
s
    forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l' Term' (UTerm TypeF IntVar)
t' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
s) (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
expected UTerm TypeF IntVar
actual)

-- ~~~~ Note [Checking and inference for record literals]
--
-- We need to handle record literals in both inference and checking
-- mode.  By way of contrast, with a pair, if we are in checking
-- mode and the expected type is not manifestly a product type, we
-- can just generate fresh unification variables for the types of
-- the two components, generate a constraint that the expected type
-- is equal to a product type of these two fresh types, and continue
-- in checking mode on both sides.  With records, however, we cannot
-- do that; if we are checking a record and the expected type is not
-- manifestly a record type, we must simply switch into inference
-- mode.  However, it is still helpful to be able to handle records
-- in checking mode too, since if we know a record type it is
-- helpful to be able to push the field types down into the fields.

------------------------------------------------------------
-- Special atomic checking

-- | Ensure a term is a valid argument to @atomic@.  Valid arguments
--   may not contain @def@, @let@, or lambda. Any variables which are
--   referenced must have a primitive, first-order type such as
--   @text@ or @int@ (in particular, no functions, @cmd@, or
--   @delay@).  We simply assume that any locally bound variables are
--   OK without checking their type: the only way to bind a variable
--   locally is with a binder of the form @x <- c1; c2@, where @c1@ is
--   some primitive command (since we can't refer to external
--   variables of type @cmd a@).  If we wanted to do something more
--   sophisticated with locally bound variables we would have to
--   inline this analysis into typechecking proper, instead of having
--   it be a separate, out-of-band check.
--
--   The goal is to ensure that any argument to @atomic@ is guaranteed
--   to evaluate and execute in some small, finite amount of time, so
--   that it's impossible to write a term which runs atomically for an
--   indefinite amount of time and freezes the rest of the game.  Of
--   course, nothing prevents one from writing a large amount of code
--   inside an @atomic@ block; but we want the execution time to be
--   linear in the size of the code.
--
--   We also ensure that the atomic block takes at most one tick,
--   i.e. contains at most one tangible command. For example, @atomic
--   (move; move)@ is invalid, since that would allow robots to move
--   twice as fast as usual by doing both actions in one tick.
validAtomic :: Syntax -> TC ()
validAtomic :: Syntax -> TC ()
validAtomic s :: Syntax
s@(Syntax SrcLoc
l Term
t) = do
  Int
n <- Set Var -> Syntax -> TC Int
analyzeAtomic forall a. Set a
S.empty Syntax
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$ forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic (Int -> InvalidAtomicReason
TooManyTicks Int
n) Term
t

-- | Analyze an argument to @atomic@: ensure it contains no nested
--   atomic blocks and no references to external variables, and count
--   how many tangible commands it will execute.
analyzeAtomic :: Set Var -> Syntax -> TC Int
analyzeAtomic :: Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals (Syntax SrcLoc
l Term
t) = case Term
t of
  -- Literals, primitives, etc. that are fine and don't require a tick
  -- to evaluate
  TUnit {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TDir {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TAntiInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TAntiText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TBool {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRobot {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRequireDevice {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRequire {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  SRequirements {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  -- Constants.
  TConst Const
c
    -- Nested 'atomic' is not allowed.
    | Const
c forall a. Eq a => a -> a -> Bool
== Const
Atomic -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
NestedAtomic Term
t
    -- We cannot allow long commands (commands that may require more
    -- than one tick to execute) since that could freeze the game.
    | Const -> Bool
isLong Const
c -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
LongConst Term
t
    -- Otherwise, return 1 or 0 depending on whether the command is
    -- tangible.
    | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Const -> Bool
isTangible Const
c then Int
1 else Int
0
  -- Special case for if: number of tangible commands is the *max* of
  -- the branches instead of the sum, since exactly one of them will be
  -- executed.
  TConst Const
If :$: Syntax
tst :$: Syntax
thn :$: Syntax
els ->
    forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
tst forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Ord a => a -> a -> a
max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
thn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
els)
  -- Pairs, application, and delay are simple: just recurse and sum the results.
  SPair Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s2
  SApp Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s2
  SDelay DelayType
_ Syntax
s1 -> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1
  -- Bind is similarly simple except that we have to keep track of a local variable
  -- bound in the RHS.
  SBind Maybe LocVar
mx Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a. Ord a => a -> Set a -> Set a
S.insert forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx Set Var
locals) Syntax
s2
  SRcd Map Var (Maybe Syntax)
m -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, Maybe Syntax) -> TC Int
analyzeField (forall k a. Map k a -> [(k, a)]
M.assocs Map Var (Maybe Syntax)
m)
   where
    analyzeField :: (Var, Maybe Syntax) -> TC Int
    analyzeField :: (Var, Maybe Syntax) -> TC Int
analyzeField (Var
x, Maybe Syntax
Nothing) = Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x))
    analyzeField (Var
_, Just Syntax
s) = Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s
  SProj {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  -- Variables are allowed if bound locally, or if they have a simple type.
  TVar Var
x
    | Var
x forall a. Ord a => a -> Set a -> Bool
`S.member` Set Var
locals -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    | Bool
otherwise -> do
        Maybe UPolytype
mxTy <- forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TC UCtx
getCtx
        case Maybe UPolytype
mxTy of
          -- If the variable is undefined, return 0 to indicate the
          -- atomic block is valid, because we'd rather have the error
          -- caught by the real name+type checking.
          Maybe UPolytype
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
          Just UPolytype
xTy -> do
            -- Use applyBindings to make sure that we apply as much
            -- information as unification has learned at this point.  In
            -- theory, continuing to typecheck other terms elsewhere in
            -- the program could give us further information about xTy,
            -- so we might have incomplete information at this point.
            -- However, since variables referenced in an atomic block
            -- must necessarily have simple types, it's unlikely this
            -- will really make a difference.  The alternative, more
            -- "correct" way to do this would be to simply emit some
            -- constraints at this point saying that xTy must be a
            -- simple type, and check later that the constraint holds,
            -- after performing complete type inference.  However, since
            -- the current approach is much simpler, we'll stick with
            -- this until such time as we have concrete examples showing
            -- that the more correct, complex way is necessary.
            UPolytype
xTy' <- forall u. HasBindings u => u -> TC u
applyBindings UPolytype
xTy
            if UPolytype -> Bool
isSimpleUPolytype UPolytype
xTy'
              then forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
              else forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic (Var -> UPolytype -> InvalidAtomicReason
NonSimpleVarType Var
x UPolytype
xTy') Term
t
  -- No lambda, `let` or `def` allowed!
  SLam {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
  SLet {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
  SDef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
  -- We should never encounter a TRef since they do not show up in
  -- surface syntax, only as values while evaluating (*after*
  -- typechecking).
  TRef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInfer Term
t
  -- An explicit type annotation doesn't change atomicity
  SAnnotate Syntax
s Polytype
_ -> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s

-- | A simple polytype is a simple type with no quantifiers.
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype (Forall [] UTerm TypeF IntVar
ty) = UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty
isSimpleUPolytype UPolytype
_ = Bool
False

-- | A simple type is a sum or product of base types.
isSimpleUType :: UType -> Bool
isSimpleUType :: UTerm TypeF IntVar -> Bool
isSimpleUType = \case
  UTyBase {} -> Bool
True
  UTyVar {} -> Bool
False
  UTySum UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2 -> UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty1 Bool -> Bool -> Bool
&& UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty2
  UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2 -> UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty1 Bool -> Bool -> Bool
&& UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty2
  UTyFun {} -> Bool
False
  UTyCmd {} -> Bool
False
  UTyDelay {} -> Bool
False
  -- Make the pattern-match coverage checker happy
  UVar {} -> Bool
False
  UTerm {} -> Bool
False