{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}

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

  -- * Typechecking monad
  fresh,

  -- * Unification
  instantiate,
  skolemize,
  generalize,

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

import Control.Arrow ((***))
import Control.Carrier.Error.Either (ErrorC, runError)
import Control.Carrier.Reader (ReaderC, runReader)
import Control.Carrier.Throw.Either (ThrowC, runThrow)
import Control.Category ((>>>))
import Control.Effect.Catch (Catch, catchError)
import Control.Effect.Error (Error)
import Control.Effect.Reader
import Control.Effect.Throw
import Control.Lens ((^.))
import Control.Lens.Indexed (itraverse)
import Control.Monad (forM_, void, when, (<=<), (>=>))
import Control.Monad.Free (Free (..))
import Data.Data (Data, gmapM)
import Data.Foldable (fold, traverse_)
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.Effect.Unify (Unification, UnificationError, (=:=))
import Swarm.Effect.Unify qualified as U
import Swarm.Effect.Unify.Fast qualified as U
import Swarm.Language.Context hiding (lookup)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Kindcheck (KindError, checkKind, checkPolytypeKind)
import Swarm.Language.Parser.QQ (tyQ)
import Swarm.Language.Requirements.Analysis (requirements)
import Swarm.Language.Requirements.Type (ReqCtx)
import Swarm.Language.Syntax
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.
  TCLet :: 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
(Int -> TCFrame -> ShowS)
-> (TCFrame -> String) -> ([TCFrame] -> ShowS) -> Show TCFrame
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TCFrame -> ShowS
showsPrec :: Int -> TCFrame -> ShowS
$cshow :: TCFrame -> String
show :: TCFrame -> String
$cshowList :: [TCFrame] -> ShowS
showList :: [TCFrame] -> ShowS
Show)

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

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

-- | Push a frame on the typechecking stack.
withFrame :: Has (Reader TCStack) sig m => SrcLoc -> TCFrame -> m a -> m a
withFrame :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l TCFrame
f = ([LocatedTCFrame] -> [LocatedTCFrame]) -> m a -> m a
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader r) sig m =>
(r -> r) -> m a -> m a
local (SrcLoc -> TCFrame -> LocatedTCFrame
LocatedTCFrame SrcLoc
l TCFrame
f LocatedTCFrame -> [LocatedTCFrame] -> [LocatedTCFrame]
forall a. a -> [a] -> [a]
:)

------------------------------------------------------------
-- 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
(Int -> Source -> ShowS)
-> (Source -> String) -> ([Source] -> ShowS) -> Show Source
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Source -> ShowS
showsPrec :: Int -> Source -> ShowS
$cshow :: Source -> String
show :: Source -> String
$cshowList :: [Source] -> ShowS
showList :: [Source] -> ShowS
Show, Source -> Source -> Bool
(Source -> Source -> Bool)
-> (Source -> Source -> Bool) -> Eq Source
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Source -> Source -> Bool
== :: Source -> Source -> Bool
$c/= :: Source -> Source -> Bool
/= :: Source -> Source -> Bool
Eq, Eq Source
Eq Source =>
(Source -> Source -> Ordering)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Source)
-> (Source -> Source -> Source)
-> Ord 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
$ccompare :: Source -> Source -> Ordering
compare :: Source -> Source -> Ordering
$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
>= :: Source -> Source -> Bool
$cmax :: Source -> Source -> Source
max :: Source -> Source -> Source
$cmin :: Source -> Source -> Source
min :: Source -> Source -> Source
Ord, Source
Source -> Source -> Bounded Source
forall a. a -> a -> Bounded a
$cminBound :: Source
minBound :: Source
$cmaxBound :: Source
maxBound :: Source
Bounded, Int -> Source
Source -> Int
Source -> [Source]
Source -> Source
Source -> Source -> [Source]
Source -> Source -> Source -> [Source]
(Source -> Source)
-> (Source -> Source)
-> (Int -> Source)
-> (Source -> Int)
-> (Source -> [Source])
-> (Source -> Source -> [Source])
-> (Source -> Source -> [Source])
-> (Source -> Source -> Source -> [Source])
-> Enum 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
$csucc :: Source -> Source
succ :: Source -> Source
$cpred :: Source -> Source
pred :: Source -> Source
$ctoEnum :: Int -> Source
toEnum :: Int -> Source
$cfromEnum :: Source -> Int
fromEnum :: Source -> Int
$cenumFrom :: Source -> [Source]
enumFrom :: Source -> [Source]
$cenumFromThen :: Source -> Source -> [Source]
enumFromThen :: Source -> Source -> [Source]
$cenumFromTo :: Source -> Source -> [Source]
enumFromTo :: Source -> Source -> [Source]
$cenumFromThenTo :: Source -> Source -> Source -> [Source]
enumFromThenTo :: Source -> Source -> 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)
  deriving ((forall a b. (a -> b) -> Join a -> Join b)
-> (forall a b. a -> Join b -> Join a) -> Functor Join
forall a b. a -> Join b -> Join a
forall a b. (a -> b) -> Join a -> Join b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Join a -> Join b
fmap :: forall a b. (a -> b) -> Join a -> Join b
$c<$ :: forall a b. a -> Join b -> Join a
<$ :: forall a b. a -> Join b -> Join a
Functor)

instance Foldable Join where
  foldMap :: Monoid m => (a -> m) -> Join a -> m
  foldMap :: forall m a. Monoid m => (a -> m) -> Join a -> m
foldMap a -> m
f Join a
j = a -> m
f a
a1 m -> m -> m
forall a. Semigroup a => a -> a -> a
<> a -> m
f a
a2
   where
    (a
a1, a
a2) = Join a -> (a, a)
forall a. Join a -> (a, a)
getJoin Join a
j

instance Traversable Join where
  traverse :: Applicative f => (a -> f b) -> Join a -> f (Join b)
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Join a -> f (Join b)
traverse a -> f b
f Join a
j = b -> b -> Join b
forall a. a -> a -> Join a
joined (b -> b -> Join b) -> f b -> f (b -> Join b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a1 f (b -> Join b) -> f b -> f (Join b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
a2
   where
    (a
a1, a
a2) = Join a -> (a, a)
forall a. Join a -> (a, a)
getJoin Join a
j

instance (Show a) => Show (Join a) where
  show :: Join a -> String
show (Join a -> (a, a)
forall a. Join a -> (a, a)
getJoin -> (a
e, a
a)) = String
"(expected: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
e String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", actual: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
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 = (Source -> a) -> Join a
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 = (Source -> a) -> Join a
forall a. (Source -> a) -> Join a
Join ((Source -> a) -> Join a) -> (Source -> a) -> Join a
forall a b. (a -> b) -> a -> b
$ \Source
s -> if Source
s Source -> Source -> Bool
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

fromUSyntax ::
  ( Has Unification sig m
  , Has (Reader UCtx) sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  USyntax ->
  m TSyntax
fromUSyntax :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
USyntax -> m TSyntax
fromUSyntax = (UType -> m Polytype) -> USyntax -> m TSyntax
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Syntax' a -> m (Syntax' b)
mapM (Maybe Polytype -> m Polytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw ContextualTypeErr) sig m =>
Maybe a -> m a
checkPredicative (Maybe Polytype -> m Polytype)
-> (UType -> m (Maybe Polytype)) -> UType -> m Polytype
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ((UPolytype -> Maybe Polytype) -> m UPolytype -> m (Maybe Polytype)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap U Polytype -> Maybe Polytype
UPolytype -> Maybe Polytype
forall t. WithU t => U t -> Maybe t
fromU (m UPolytype -> m (Maybe Polytype))
-> (UType -> m UPolytype) -> UType -> m (Maybe Polytype)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UType -> m UPolytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m) =>
UType -> m UPolytype
generalize))

finalizeUSyntax ::
  ( Has Unification sig m
  , Has (Reader UCtx) sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  USyntax ->
  m TSyntax
finalizeUSyntax :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
USyntax -> m TSyntax
finalizeUSyntax = USyntax -> m USyntax
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
USyntax -> m USyntax
applyBindings (USyntax -> m USyntax)
-> (USyntax -> m TSyntax) -> USyntax -> m TSyntax
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> USyntax -> m TSyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
USyntax -> m TSyntax
fromUSyntax

-- | Version of 'runTC' which is generic in the base monad.
runTC' ::
  Algebra sig m =>
  TCtx ->
  ReqCtx ->
  TDCtx ->
  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx m))))) USyntax ->
  m (Either ContextualTypeErr TSyntax)
runTC' :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Algebra sig m =>
TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     USyntax
-> m (Either ContextualTypeErr TSyntax)
runTC' TCtx
ctx Ctx Requirements
reqCtx Ctx TydefInfo
tdctx =
  (ReaderC
  UCtx
  (ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
  USyntax
-> (USyntax
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
         TSyntax)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     TSyntax
forall a b.
ReaderC
  UCtx
  (ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
  a
-> (a
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
         b)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= USyntax
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     TSyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
USyntax -> m TSyntax
finalizeUSyntax)
    (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
   USyntax
 -> ReaderC
      UCtx
      (ReaderC
         [LocatedTCFrame]
         (ErrorC
            ContextualTypeErr
            (UnificationC
               (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
      TSyntax)
-> (ReaderC
      UCtx
      (ReaderC
         [LocatedTCFrame]
         (ErrorC
            ContextualTypeErr
            (UnificationC
               (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     USyntax
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> UCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     TSyntax
-> ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
     TSyntax
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader (TCtx -> U TCtx
forall t. WithU t => t -> U t
toU TCtx
ctx)
    (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
   TSyntax
 -> ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
      TSyntax)
-> (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     TSyntax
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> [LocatedTCFrame]
-> ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
     TSyntax
-> ErrorC
     ContextualTypeErr
     (UnificationC
        (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
     TSyntax
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader []
    (ReaderC
   [LocatedTCFrame]
   (ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
   TSyntax
 -> ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
      TSyntax)
-> (ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))))
     TSyntax
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ErrorC
  ContextualTypeErr
  (UnificationC
     (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
  TSyntax
-> UnificationC
     (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
     (Either ContextualTypeErr TSyntax)
forall exc (m :: * -> *) a. ErrorC exc m a -> m (Either exc a)
runError
    (ErrorC
   ContextualTypeErr
   (UnificationC
      (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
   TSyntax
 -> UnificationC
      (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
      (Either ContextualTypeErr TSyntax))
-> (UnificationC
      (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
      (Either ContextualTypeErr TSyntax)
    -> m (Either ContextualTypeErr TSyntax))
-> ErrorC
     ContextualTypeErr
     (UnificationC
        (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))
     TSyntax
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> UnificationC
  (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
  (Either ContextualTypeErr TSyntax)
-> ReaderC
     (Ctx Requirements)
     (ReaderC (Ctx TydefInfo) m)
     (Either UnificationError (Either ContextualTypeErr TSyntax))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Algebra sig m, Has (Reader (Ctx TydefInfo)) sig m) =>
UnificationC m a -> m (Either UnificationError a)
U.runUnification
    (UnificationC
   (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
   (Either ContextualTypeErr TSyntax)
 -> ReaderC
      (Ctx Requirements)
      (ReaderC (Ctx TydefInfo) m)
      (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (ReaderC
      (Ctx Requirements)
      (ReaderC (Ctx TydefInfo) m)
      (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> UnificationC
     (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m))
     (Either ContextualTypeErr TSyntax)
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Ctx Requirements
-> ReaderC
     (Ctx Requirements)
     (ReaderC (Ctx TydefInfo) m)
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> ReaderC
     (Ctx TydefInfo)
     m
     (Either UnificationError (Either ContextualTypeErr TSyntax))
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader Ctx Requirements
reqCtx
    (ReaderC
   (Ctx Requirements)
   (ReaderC (Ctx TydefInfo) m)
   (Either UnificationError (Either ContextualTypeErr TSyntax))
 -> ReaderC
      (Ctx TydefInfo)
      m
      (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (ReaderC
      (Ctx TydefInfo)
      m
      (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     (Ctx Requirements)
     (ReaderC (Ctx TydefInfo) m)
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Ctx TydefInfo
-> ReaderC
     (Ctx TydefInfo)
     m
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> m (Either UnificationError (Either ContextualTypeErr TSyntax))
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader Ctx TydefInfo
tdctx
    (ReaderC
   (Ctx TydefInfo)
   m
   (Either UnificationError (Either ContextualTypeErr TSyntax))
 -> m (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (m (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     (Ctx TydefInfo)
     m
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> m (Either ContextualTypeErr TSyntax)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (Either UnificationError (Either ContextualTypeErr TSyntax)
 -> Either ContextualTypeErr TSyntax)
-> m (Either UnificationError (Either ContextualTypeErr TSyntax))
-> m (Either ContextualTypeErr TSyntax)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either UnificationError (Either ContextualTypeErr TSyntax)
-> Either ContextualTypeErr TSyntax
forall a.
Either UnificationError (Either ContextualTypeErr a)
-> Either ContextualTypeErr a
reportUnificationError

-- | Run a top-level inference computation, returning either a
--   'ContextualTypeErr' or a fully resolved 'TSyntax'.
runTC ::
  TCtx ->
  ReqCtx ->
  TDCtx ->
  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx Identity))))) USyntax ->
  Either ContextualTypeErr TSyntax
runTC :: TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
     USyntax
-> Either ContextualTypeErr TSyntax
runTC TCtx
tctx Ctx Requirements
reqCtx Ctx TydefInfo
tdctx = TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
     USyntax
-> Identity (Either ContextualTypeErr TSyntax)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Algebra sig m =>
TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) m)))))
     USyntax
-> m (Either ContextualTypeErr TSyntax)
runTC' TCtx
tctx Ctx Requirements
reqCtx Ctx TydefInfo
tdctx (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
   USyntax
 -> Identity (Either ContextualTypeErr TSyntax))
-> (Identity (Either ContextualTypeErr TSyntax)
    -> Either ContextualTypeErr TSyntax)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
     USyntax
-> Either ContextualTypeErr TSyntax
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Identity (Either ContextualTypeErr TSyntax)
-> Either ContextualTypeErr TSyntax
forall a. Identity a -> a
runIdentity

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

reportUnificationError :: Either UnificationError (Either ContextualTypeErr a) -> Either ContextualTypeErr a
reportUnificationError :: forall a.
Either UnificationError (Either ContextualTypeErr a)
-> Either ContextualTypeErr a
reportUnificationError = (UnificationError -> Either ContextualTypeErr a)
-> (Either ContextualTypeErr a -> Either ContextualTypeErr a)
-> Either UnificationError (Either ContextualTypeErr a)
-> Either ContextualTypeErr a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ContextualTypeErr -> Either ContextualTypeErr a
forall a b. a -> Either a b
Left (ContextualTypeErr -> Either ContextualTypeErr a)
-> (UnificationError -> ContextualTypeErr)
-> UnificationError
-> Either ContextualTypeErr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeErr -> ContextualTypeErr
mkRawTypeErr (TypeErr -> ContextualTypeErr)
-> (UnificationError -> TypeErr)
-> UnificationError
-> ContextualTypeErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnificationError -> TypeErr
UnificationErr) Either ContextualTypeErr a -> Either ContextualTypeErr a
forall a. a -> a
id

-- | 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 ::
  ( Has (Throw ContextualTypeErr) sig m
  , Has (Reader TCStack) sig m
  , Has (Reader UCtx) sig m
  , Has Unification sig m
  ) =>
  SrcLoc ->
  Var ->
  m UType
lookup :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has (Reader UCtx) sig m,
 Has Unification sig m) =>
SrcLoc -> Var -> m UType
lookup SrcLoc
loc Var
x = do
  UCtx
ctx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @UCtx
  m UType -> (UPolytype -> m UType) -> Maybe UPolytype -> m UType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SrcLoc -> TypeErr -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
loc (TypeErr -> m UType) -> TypeErr -> m UType
forall a b. (a -> b) -> a -> b
$ Var -> TypeErr
UnboundVar Var
x) UPolytype -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
instantiate (Var -> UCtx -> Maybe UPolytype
forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x UCtx
ctx)

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

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

-- | A class for getting the free unification variables of a thing.
class FreeUVars a where
  freeUVars :: Has Unification sig m => a -> m (Set IntVar)

-- | We can get the free unification variables of a 'UType'.
instance FreeUVars UType where
  freeUVars :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m (Set IntVar)
freeUVars = UType -> m (Set IntVar)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m (Set IntVar)
U.freeUVars

-- | We can also get the free variables of a polytype.
instance (FreeUVars t) => FreeUVars (Poly t) where
  freeUVars :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
Poly t -> m (Set IntVar)
freeUVars (Forall [Var]
_ t
t) = t -> m (Set IntVar)
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
(FreeUVars a, Has Unification sig m) =>
a -> m (Set IntVar)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
t -> m (Set IntVar)
freeUVars t
t

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

-- | Generate a fresh unification variable.
fresh :: Has Unification sig m => m UType
fresh :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh = IntVar -> UType
forall (f :: * -> *) a. a -> Free f a
Pure (IntVar -> UType) -> m IntVar -> m UType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m IntVar
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m IntVar
U.freshIntVar

-- | 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) UType -> UType -> UType
substU Map (Either Var IntVar) UType
m =
  (IntVar -> UType) -> (TypeF UType -> UType) -> UType -> UType
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata
    (\IntVar
v -> UType -> Maybe UType -> UType
forall a. a -> Maybe a -> a
fromMaybe (IntVar -> UType
forall (f :: * -> *) a. a -> Free f a
Pure IntVar
v) (Either Var IntVar -> Map (Either Var IntVar) UType -> Maybe UType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (IntVar -> Either Var IntVar
forall a b. b -> Either a b
Right IntVar
v) Map (Either Var IntVar) UType
m))
    ( \case
        TyVarF Var
v -> UType -> Maybe UType -> UType
forall a. a -> Maybe a -> a
fromMaybe (Var -> UType
UTyVar Var
v) (Either Var IntVar -> Map (Either Var IntVar) UType -> Maybe UType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Var -> Either Var IntVar
forall a b. a -> Either a b
Left Var
v) Map (Either Var IntVar) UType
m)
        TypeF UType
f -> TypeF UType -> UType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free TypeF UType
f
    )

-- | Make sure no skolem variables escape.
noSkolems ::
  ( Has Unification sig m
  , Has (Reader TCStack) sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  SrcLoc ->
  Poly UType ->
  m ()
noSkolems :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> UPolytype -> m ()
noSkolems SrcLoc
l (Forall [Var]
xs UType
upty) = do
  UType
upty' <- UType -> m UType
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings UType
upty
  let tyvs :: Set Var
tyvs =
        (IntVar -> Set Var)
-> (TypeF (Set Var) -> Set Var) -> UType -> Set Var
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> Free t v -> a
ucata
          (Set Var -> IntVar -> Set Var
forall a b. a -> b -> a
const Set Var
forall a. Set a
S.empty)
          (\case TyVarF Var
v -> Var -> Set Var
forall a. a -> Set a
S.singleton Var
v; TypeF (Set Var)
f -> TypeF (Set Var) -> Set Var
forall m. Monoid m => TypeF m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)
          UType
upty'
      ftyvs :: Set Var
ftyvs = Set Var
tyvs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
  Maybe Var -> (Var -> m Any) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set Var -> Maybe Var
forall a. Set a -> Maybe a
S.lookupMin Set Var
ftyvs) ((Var -> m Any) -> m ()) -> (Var -> m Any) -> m ()
forall a b. (a -> b) -> a -> b
$ SrcLoc -> TypeErr -> m Any
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Any) -> (Var -> TypeErr) -> Var -> m Any
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.

-- | @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.
unify ::
  ( Has Unification sig m
  , Has (Throw ContextualTypeErr) sig m
  , Has (Reader TCStack) sig m
  ) =>
  Maybe Syntax ->
  TypeJoin ->
  m UType
unify :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Maybe Syntax -> TypeJoin -> m UType
unify Maybe Syntax
ms TypeJoin
j = do
  Either UnificationError UType
res <- UType
expected UType -> UType -> m (Either UnificationError UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> UType -> m (Either UnificationError UType)
=:= UType
actual
  case Either UnificationError UType
res of
    Left UnificationError
_ -> do
      TypeJoin
j' <- (UType -> m UType) -> TypeJoin -> m TypeJoin
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Join a -> f (Join b)
traverse UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
U.applyBindings TypeJoin
j
      SrcLoc -> TypeErr -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
NoLoc (TypeErr -> m UType) -> TypeErr -> m UType
forall a b. (a -> b) -> a -> b
$ Maybe Syntax -> TypeJoin -> TypeErr
Mismatch Maybe Syntax
ms TypeJoin
j'
    Right UType
ty -> UType -> m UType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
ty
 where
  (UType
expected, UType
actual) = TypeJoin -> (UType, UType)
forall a. Join a -> (a, a)
getJoin TypeJoin
j

-- | The 'HasBindings' class is for anything which has
--   unification variables in it and to which we can usefully apply
--   'applyBindings'.
class HasBindings u where
  applyBindings :: Has Unification sig m => u -> m u

instance HasBindings UType where
  applyBindings :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings = UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
U.applyBindings

instance HasBindings UPolytype where
  applyBindings :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UPolytype
applyBindings (Forall [Var]
xs UType
u) = [Var] -> UType -> UPolytype
forall t. [Var] -> t -> Poly t
Forall [Var]
xs (UType -> UPolytype) -> m UType -> m UPolytype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UType -> m UType
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings UType
u

instance HasBindings UCtx where
  applyBindings :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UCtx -> m UCtx
applyBindings = (UPolytype -> m UPolytype) -> UCtx -> m UCtx
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ctx a -> m (Ctx b)
mapM UPolytype -> m UPolytype
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UPolytype
applyBindings

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

instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
  applyBindings :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
Syntax' u -> m (Syntax' u)
applyBindings (Syntax' SrcLoc
l Term' u
t Comments
cs u
u) = SrcLoc -> Term' u -> Comments -> u -> Syntax' u
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Term' u -> Comments -> u -> Syntax' u)
-> m (Term' u) -> m (Comments -> u -> Syntax' u)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term' u -> m (Term' u)
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
Term' u -> m (Term' u)
applyBindings Term' u
t m (Comments -> u -> Syntax' u) -> m Comments -> m (u -> Syntax' u)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Comments -> m Comments
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Comments
cs m (u -> Syntax' u) -> m u -> m (Syntax' u)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> u -> m u
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
u -> m u
applyBindings u
u

------------------------------------------------------------
-- 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 :: Has Unification sig m => UPolytype -> m UType
instantiate :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
instantiate (Forall [Var]
xs UType
uty) = do
  [UType]
xs' <- (Var -> m UType) -> [Var] -> m [UType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m UType -> Var -> m UType
forall a b. a -> b -> a
const m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh) [Var]
xs
  UType -> m UType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UType -> m UType) -> UType -> m UType
forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) UType -> UType -> UType
substU ([(Either Var IntVar, UType)] -> Map (Either Var IntVar) UType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Either Var IntVar] -> [UType] -> [(Either Var IntVar, UType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Var -> Either Var IntVar) -> [Var] -> [Either Var IntVar]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Either Var IntVar
forall a b. a -> Either a b
Left [Var]
xs) [UType]
xs')) UType
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 :: Has Unification sig m => UPolytype -> m UType
skolemize :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
skolemize (Forall [Var]
xs UType
uty) = do
  [UType]
xs' <- (Var -> m UType) -> [Var] -> m [UType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (m UType -> Var -> m UType
forall a b. a -> b -> a
const m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh) [Var]
xs
  UType -> m UType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UType -> m UType) -> UType -> m UType
forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) UType -> UType -> UType
substU ([(Either Var IntVar, UType)] -> Map (Either Var IntVar) UType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Either Var IntVar] -> [UType] -> [(Either Var IntVar, UType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Var -> Either Var IntVar) -> [Var] -> [Either Var IntVar]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Either Var IntVar
forall a b. a -> Either a b
Left [Var]
xs) ((UType -> UType) -> [UType] -> [UType]
forall a b. (a -> b) -> [a] -> [b]
map UType -> UType
forall {f :: * -> *}. Show1 f => Free f IntVar -> UType
toSkolem [UType]
xs'))) UType
uty
 where
  toSkolem :: Free f IntVar -> UType
toSkolem (Pure IntVar
v) = Var -> UType
UTyVar (Var -> IntVar -> Var
mkVarName Var
"s" IntVar
v)
  toSkolem Free f IntVar
x = String -> UType
forall a. HasCallStack => String -> a
error (String -> UType) -> String -> UType
forall a b. (a -> b) -> a -> b
$ String
"Impossible! Non-UVar in skolemize.toSkolem: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Free f IntVar -> String
forall a. Show a => a -> String
show Free f 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 :: (Has Unification sig m, Has (Reader UCtx) sig m) => UType -> m UPolytype
generalize :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m) =>
UType -> m UPolytype
generalize UType
uty = do
  UType
uty' <- UType -> m UType
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings UType
uty
  UCtx
ctx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @UCtx
  Set IntVar
tmfvs <- UType -> m (Set IntVar)
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
(FreeUVars a, Has Unification sig m) =>
a -> m (Set IntVar)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m (Set IntVar)
freeUVars UType
uty'
  Set IntVar
ctxfvs <- UCtx -> m (Set IntVar)
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
(FreeUVars a, Has Unification sig m) =>
a -> m (Set IntVar)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UCtx -> m (Set IntVar)
freeUVars UCtx
ctx
  let fvs :: [IntVar]
fvs = Set IntVar -> [IntVar]
forall a. Set a -> [a]
S.toList (Set IntVar -> [IntVar]) -> Set IntVar -> [IntVar]
forall a b. (a -> b) -> a -> b
$ Set IntVar
tmfvs Set IntVar -> Set IntVar -> Set IntVar
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 = (String -> Var) -> [String] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map String -> Var
T.pack ((Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> ShowS
forall a. a -> [a] -> [a]
: []) String
alphabet [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Char
x Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
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 = [IntVar] -> [Var] -> [(IntVar, Var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [IntVar]
fvs [Var]
prettyNames
  UPolytype -> m UPolytype
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype -> m UPolytype) -> UPolytype -> m UPolytype
forall a b. (a -> b) -> a -> b
$
    [Var] -> UType -> UPolytype
forall t. [Var] -> t -> Poly t
Forall
      (((IntVar, Var) -> Var) -> [(IntVar, Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (IntVar, Var) -> Var
forall a b. (a, b) -> b
snd [(IntVar, Var)]
renaming)
      (Map (Either Var IntVar) UType -> UType -> UType
substU ([(Either Var IntVar, UType)] -> Map (Either Var IntVar) UType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Either Var IntVar, UType)] -> Map (Either Var IntVar) UType)
-> ([(IntVar, Var)] -> [(Either Var IntVar, UType)])
-> [(IntVar, Var)]
-> Map (Either Var IntVar) UType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IntVar, Var) -> (Either Var IntVar, UType))
-> [(IntVar, Var)] -> [(Either Var IntVar, UType)]
forall a b. (a -> b) -> [a] -> [b]
map (IntVar -> Either Var IntVar
forall a b. b -> Either a b
Right (IntVar -> Either Var IntVar)
-> (Var -> UType) -> (IntVar, Var) -> (Either Var IntVar, UType)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Var -> UType
UTyVar) ([(IntVar, Var)] -> Map (Either Var IntVar) UType)
-> [(IntVar, Var)] -> Map (Either Var IntVar) UType
forall a b. (a -> b) -> a -> b
$ [(IntVar, Var)]
renaming) UType
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 -> [LocatedTCFrame]
cteStack :: TCStack, ContextualTypeErr -> TypeErr
cteTypeErr :: TypeErr}
  deriving (Int -> ContextualTypeErr -> ShowS
[ContextualTypeErr] -> ShowS
ContextualTypeErr -> String
(Int -> ContextualTypeErr -> ShowS)
-> (ContextualTypeErr -> String)
-> ([ContextualTypeErr] -> ShowS)
-> Show ContextualTypeErr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ContextualTypeErr -> ShowS
showsPrec :: Int -> ContextualTypeErr -> ShowS
$cshow :: ContextualTypeErr -> String
show :: ContextualTypeErr -> String
$cshowList :: [ContextualTypeErr] -> ShowS
showList :: [ContextualTypeErr] -> ShowS
Show)

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

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

-- | Throw a 'ContextualTypeErr'.
throwTypeErr ::
  ( Has (Throw ContextualTypeErr) sig m
  , Has (Reader TCStack) sig m
  ) =>
  SrcLoc ->
  TypeErr ->
  m a
throwTypeErr :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l TypeErr
te = do
  [LocatedTCFrame]
stk <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TCStack
  ContextualTypeErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError (ContextualTypeErr -> m a) -> ContextualTypeErr -> m a
forall a b. (a -> b) -> a -> b
$ SrcLoc -> [LocatedTCFrame] -> TypeErr -> ContextualTypeErr
mkTypeErr SrcLoc
l [LocatedTCFrame]
stk TypeErr
te

-- | Adapt some other error type to a 'ContextualTypeErr'.
adaptToTypeErr ::
  ( Has (Throw ContextualTypeErr) sig m
  , Has (Reader TCStack) sig m
  ) =>
  SrcLoc ->
  (e -> TypeErr) ->
  ThrowC e m a ->
  m a
adaptToTypeErr :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l e -> TypeErr
adapt ThrowC e m a
m = do
  Either e a
res <- ThrowC e m a -> m (Either e a)
forall e (m :: * -> *) a. ThrowC e m a -> m (Either e a)
runThrow ThrowC e m a
m
  case Either e a
res of
    Left e
e -> SrcLoc -> TypeErr -> m a
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (e -> TypeErr
adapt e
e)
    Right a
a -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | 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 kind error was encountered.
    KindErr KindError
  | -- | A Skolem variable escaped its local context.
    EscapedSkolem Var
  | -- | Occurs check failure, i.e. infinite type.
    UnificationErr UnificationError
  | -- | Type mismatch caught by 'unify'.  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
(Int -> TypeErr -> ShowS)
-> (TypeErr -> String) -> ([TypeErr] -> ShowS) -> Show TypeErr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeErr -> ShowS
showsPrec :: Int -> TypeErr -> ShowS
$cshow :: TypeErr -> String
show :: TypeErr -> String
$cshowList :: [TypeErr] -> ShowS
showList :: [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
  | -- | The argument contained a suspend
    AtomicSuspend
  deriving (Int -> InvalidAtomicReason -> ShowS
[InvalidAtomicReason] -> ShowS
InvalidAtomicReason -> String
(Int -> InvalidAtomicReason -> ShowS)
-> (InvalidAtomicReason -> String)
-> ([InvalidAtomicReason] -> ShowS)
-> Show InvalidAtomicReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InvalidAtomicReason -> ShowS
showsPrec :: Int -> InvalidAtomicReason -> ShowS
$cshow :: InvalidAtomicReason -> String
show :: InvalidAtomicReason -> String
$cshowList :: [InvalidAtomicReason] -> ShowS
showList :: [InvalidAtomicReason] -> ShowS
Show)

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

-- | Decompose a type that is supposed to be the application of a
--   given type constructor to a single type argument. Also take the
--   term which is supposed to have that type, for use in error
--   messages.
decomposeTyConApp1 ::
  ( Has Unification sig m
  , Has (Throw ContextualTypeErr) sig m
  , Has (Reader TDCtx) sig m
  , Has (Reader TCStack) sig m
  ) =>
  TyCon ->
  Syntax ->
  Sourced UType ->
  m UType
decomposeTyConApp1 :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
c Syntax
t (Source
src, UTyConApp (TCUser Var
u) [UType]
as) = do
  UType
ty2 <- Var -> [UType] -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader (Ctx TydefInfo)) sig m, Typical t) =>
Var -> [t] -> m t
expandTydef Var
u [UType]
as
  TyCon -> Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
c Syntax
t (Source
src, UType
ty2)
decomposeTyConApp1 TyCon
c Syntax
_ (Source
_, UTyConApp TyCon
c' [UType
a])
  | TyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c' = UType -> m UType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
a
decomposeTyConApp1 TyCon
c Syntax
t Sourced UType
ty = do
  UType
a <- m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh
  UType
_ <- Maybe Syntax -> TypeJoin -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Maybe Syntax -> TypeJoin -> m UType
unify (Syntax -> Maybe Syntax
forall a. a -> Maybe a
Just Syntax
t) (Sourced UType -> UType -> TypeJoin
forall a. Sourced a -> a -> Join a
mkJoin Sourced UType
ty (TyCon -> [UType] -> UType
UTyConApp TyCon
c [UType
a]))
  UType -> m UType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return UType
a

decomposeCmdTy
  , decomposeDelayTy ::
    ( Has Unification sig m
    , Has (Throw ContextualTypeErr) sig m
    , Has (Reader TDCtx) sig m
    , Has (Reader TCStack) sig m
    ) =>
    Syntax ->
    Sourced UType ->
    m UType
decomposeCmdTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy = TyCon -> Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
TCCmd
decomposeDelayTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeDelayTy = TyCon -> Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
TCDelay

-- | Decompose a type that is supposed to be the application of a
--   given type constructor to two type arguments.  Also take the term
--   which is supposed to have that type, for use in error messages.
decomposeTyConApp2 ::
  ( Has Unification sig m
  , Has (Throw ContextualTypeErr) sig m
  , Has (Reader TDCtx) sig m
  , Has (Reader TCStack) sig m
  ) =>
  TyCon ->
  Syntax ->
  Sourced UType ->
  m (UType, UType)
decomposeTyConApp2 :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m (UType, UType)
decomposeTyConApp2 TyCon
c Syntax
t (Source
src, UTyConApp (TCUser Var
u) [UType]
as) = do
  UType
ty2 <- Var -> [UType] -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader (Ctx TydefInfo)) sig m, Typical t) =>
Var -> [t] -> m t
expandTydef Var
u [UType]
as
  TyCon -> Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m (UType, UType)
decomposeTyConApp2 TyCon
c Syntax
t (Source
src, UType
ty2)
decomposeTyConApp2 TyCon
c Syntax
_ (Source
_, UTyConApp TyCon
c' [UType
ty1, UType
ty2])
  | TyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c' = (UType, UType) -> m (UType, UType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UType
ty1, UType
ty2)
decomposeTyConApp2 TyCon
c Syntax
t Sourced UType
ty = do
  UType
a1 <- m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh
  UType
a2 <- m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh
  UType
_ <- Maybe Syntax -> TypeJoin -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Maybe Syntax -> TypeJoin -> m UType
unify (Syntax -> Maybe Syntax
forall a. a -> Maybe a
Just Syntax
t) (Sourced UType -> UType -> TypeJoin
forall a. Sourced a -> a -> Join a
mkJoin Sourced UType
ty (TyCon -> [UType] -> UType
UTyConApp TyCon
c [UType
a1, UType
a2]))
  (UType, UType) -> m (UType, UType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UType
a1, UType
a2)

decomposeFunTy
  , decomposeProdTy ::
    ( Has Unification sig m
    , Has (Throw ContextualTypeErr) sig m
    , Has (Reader TDCtx) sig m
    , Has (Reader TCStack) sig m
    ) =>
    Syntax ->
    Sourced UType ->
    m (UType, UType)
decomposeFunTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeFunTy = TyCon -> Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m (UType, UType)
decomposeTyConApp2 TyCon
TCFun
decomposeProdTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeProdTy = TyCon -> Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m (UType, UType)
decomposeTyConApp2 TyCon
TCProd

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

-- | Top-level type inference function: given a context of definition
--   types, type synonyms, and a term, either return a type error or a
--   fully type-annotated version of the term.
inferTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Either ContextualTypeErr TSyntax
inferTop :: TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> Syntax
-> Either ContextualTypeErr TSyntax
inferTop TCtx
ctx Ctx Requirements
reqCtx Ctx TydefInfo
tdCtx = TCtx
-> Ctx Requirements
-> Ctx TydefInfo
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
     USyntax
-> Either ContextualTypeErr TSyntax
runTC TCtx
ctx Ctx Requirements
reqCtx Ctx TydefInfo
tdCtx (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
   USyntax
 -> Either ContextualTypeErr TSyntax)
-> (Syntax
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
         USyntax)
-> Syntax
-> Either ContextualTypeErr TSyntax
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Syntax
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC (Ctx Requirements) (ReaderC (Ctx TydefInfo) Identity)))))
     USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer

-- | Infer the type of a term, 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.
--
--   Note that we choose to do kind checking inline as we go during
--   typechecking.  This has pros and cons.  The benefit is that we get
--   to piggyback on the existing source location tracking and
--   typechecking stack, so we can generate better error messages.  The
--   downside is that we have to be really careful not to miss any types
--   along the way; there is no difference, at the Haskell type level,
--   between ill- and well-kinded Swarm types, so we just have to make
--   sure that we call checkKind on every type embedded in the term
--   being checked.
infer ::
  ( Has (Reader UCtx) sig m
  , Has (Reader ReqCtx) sig m
  , Has (Reader TDCtx) sig m
  , Has (Reader TCStack) sig m
  , Has Unification sig m
  , Has (Error ContextualTypeErr) sig m
  ) =>
  Syntax ->
  m (Syntax' UType)
infer :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer s :: Syntax
s@(CSyntax SrcLoc
l Term
t Comments
cs) = SrcLoc -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Catch ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> m a -> m a
addLocToTypeErr SrcLoc
l (m USyntax -> m USyntax) -> m USyntax -> m USyntax
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 -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l Term' UType
forall ty. Term' ty
TUnit Comments
cs UType
UTyUnit
  TConst Const
c -> SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Const -> Term' UType
forall ty. Const -> Term' ty
TConst Const
c) Comments
cs (UType -> USyntax) -> m UType -> m USyntax
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UPolytype -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
instantiate (UPolytype -> m UType)
-> (Polytype -> UPolytype) -> Polytype -> m UType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polytype -> U Polytype
Polytype -> UPolytype
forall t. WithU t => t -> U t
toU (Polytype -> m UType) -> Polytype -> m UType
forall a b. (a -> b) -> a -> b
$ Const -> Polytype
inferConst Const
c)
  TDir Direction
d -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Direction -> Term' UType
forall ty. Direction -> Term' ty
TDir Direction
d) Comments
cs UType
UTyDir
  TInt Integer
n -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Integer -> Term' UType
forall ty. Integer -> Term' ty
TInt Integer
n) Comments
cs UType
UTyInt
  TAntiInt Var
x -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> Term' UType
forall ty. Var -> Term' ty
TAntiInt Var
x) Comments
cs UType
UTyInt
  TText Var
x -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> Term' UType
forall ty. Var -> Term' ty
TText Var
x) Comments
cs UType
UTyText
  TAntiText Var
x -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> Term' UType
forall ty. Var -> Term' ty
TAntiText Var
x) Comments
cs UType
UTyText
  TBool Bool
b -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Bool -> Term' UType
forall ty. Bool -> Term' ty
TBool Bool
b) Comments
cs UType
UTyBool
  TRobot Int
r -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Int -> Term' UType
forall ty. Int -> Term' ty
TRobot Int
r) Comments
cs UType
UTyActor
  TRequireDevice Var
d -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> Term' UType
forall ty. Var -> Term' ty
TRequireDevice Var
d) Comments
cs (UType -> UType
UTyCmd UType
UTyUnit)
  TRequire Int
n Var
d -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Int -> Var -> Term' UType
forall ty. Int -> Var -> Term' ty
TRequire Int
n Var
d) Comments
cs (UType -> UType
UTyCmd UType
UTyUnit)
  SRequirements Var
x Syntax
t1 -> do
    USyntax
t1' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
t1
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> USyntax -> Term' UType
forall ty. Var -> Syntax' ty -> Term' ty
SRequirements Var
x USyntax
t1') Comments
cs (UType -> UType
UTyCmd UType
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
_ -> SrcLoc -> TypeErr -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m USyntax) -> TypeErr -> m USyntax
forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInfer Term
t
  -- Just look up variables in the context.
  TVar Var
x -> SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Var -> Term' UType
forall ty. Var -> Term' ty
TVar Var
x) Comments
cs (UType -> USyntax) -> m UType -> m USyntax
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> Var -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has (Reader UCtx) sig m,
 Has Unification sig m) =>
SrcLoc -> Var -> m UType
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 Fix TypeF
argTy) Syntax
body -> do
    SrcLoc -> (KindError -> TypeErr) -> ThrowC KindError m () -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l KindError -> TypeErr
KindErr (ThrowC KindError m () -> m ()) -> ThrowC KindError m () -> m ()
forall a b. (a -> b) -> a -> b
$ Fix TypeF -> ThrowC KindError m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Ctx TydefInfo)) sig m,
 Has (Throw KindError) sig m) =>
Fix TypeF -> m ()
checkKind Fix TypeF
argTy
    let uargTy :: U (Fix TypeF)
uargTy = Fix TypeF -> U (Fix TypeF)
forall t. WithU t => t -> U t
toU Fix TypeF
argTy
    USyntax
body' <- Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) ([Var] -> UType -> UPolytype
forall t. [Var] -> t -> Poly t
Forall [] UType
uargTy) (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
body
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (LocVar -> Maybe (Fix TypeF) -> USyntax -> Term' UType
forall ty. LocVar -> Maybe (Fix TypeF) -> Syntax' ty -> Term' ty
SLam LocVar
x (Fix TypeF -> Maybe (Fix TypeF)
forall a. a -> Maybe a
Just Fix TypeF
argTy) USyntax
body') Comments
cs (UType -> UType -> UType
UTyFun UType
uargTy (USyntax
body' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' 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 Const -> [Const] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh m UType -> (UType -> m USyntax) -> m USyntax
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
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.
    USyntax
f' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
f
    (UType
argTy, UType
resTy) <- Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeFunTy Syntax
f (Source
Actual, USyntax
f' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType)

    -- Then check that the argument has the right type.
    USyntax
x' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
x UType
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`).
    UType
resTy' <- UType -> m UType
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings UType
resTy

    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> USyntax -> Term' UType
forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp USyntax
f' USyntax
x') Comments
cs UType
resTy'

  -- We handle binds in inference mode for a similar reason to
  -- application.
  --
  -- There is no way to annotate a bind with types or requirements in
  -- the surface syntax, so the second through fourth fields are
  -- necessarily Nothing.
  SBind Maybe LocVar
mx Maybe ()
_ Maybe Polytype
_ Maybe Requirements
_ Syntax
c1 Syntax
c2 -> do
    USyntax
c1' <- SrcLoc -> TCFrame -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l TCFrame
TCBindL (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
c1
    UType
a <- Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy Syntax
c1 (Source
Actual, USyntax
c1' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType)
    UPolytype
genA <- UType -> m UPolytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m) =>
UType -> m UPolytype
generalize UType
a
    USyntax
c2' <-
      (m USyntax -> m USyntax)
-> (LocVar -> m USyntax -> m USyntax)
-> Maybe LocVar
-> m USyntax
-> m USyntax
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m USyntax -> m USyntax
forall a. a -> a
id ((Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
`withBinding` UPolytype
genA) (Var -> m USyntax -> m USyntax)
-> (LocVar -> Var) -> LocVar -> m USyntax -> m USyntax
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
        (m USyntax -> m USyntax)
-> (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcLoc -> TCFrame -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l TCFrame
TCBindR
        (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer 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.
    UType
_ <- Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy Syntax
c2 (Source
Actual, USyntax
c2' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType)

    -- NOTE: it is probably not correct to say that the variable bound
    -- in a monadic bind has no requirements.  But as long as it is
    -- some kind of primitive value type (Int, Bool, etc.) it really
    -- doesn't matter, since it will already be evaluated, so using it
    -- in the future really does incur no requirements.  It would only
    -- matter if someone used something like
    --
    --   f <- (c : Cmd (Cmd Int)); ... f ...
    --
    -- so that f ends up with a type like Cmd Int.  But we already
    -- don't handle that kind of thing correctly anyway.  The real fix
    -- will have to wait for #231.
    let binderReqs :: Requirements
binderReqs = Requirements
forall a. Monoid a => a
mempty

    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Maybe LocVar
-> Maybe UType
-> Maybe Polytype
-> Maybe Requirements
-> USyntax
-> USyntax
-> Term' UType
forall ty.
Maybe LocVar
-> Maybe ty
-> Maybe Polytype
-> Maybe Requirements
-> Syntax' ty
-> Syntax' ty
-> Term' ty
SBind Maybe LocVar
mx (UType -> Maybe UType
forall a. a -> Maybe a
Just UType
a) Maybe Polytype
forall a. Maybe a
Nothing (Requirements -> Maybe Requirements
forall a. a -> Maybe a
Just Requirements
binderReqs) USyntax
c1' USyntax
c2') Comments
cs (USyntax
c2' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' 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
    USyntax
t1' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
t1
    case USyntax
t1' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType of
      UTyRcd Map Var UType
m -> case Var -> Map Var UType -> Maybe UType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var UType
m of
        Just UType
xTy -> USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> Var -> Term' UType
forall ty. Syntax' ty -> Var -> Term' ty
SProj USyntax
t1' Var
x) Comments
cs UType
xTy
        Maybe UType
Nothing -> SrcLoc -> TypeErr -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m USyntax) -> TypeErr -> m USyntax
forall a b. (a -> b) -> a -> b
$ Var -> Term -> TypeErr
UnknownProj Var
x (Syntax -> Var -> Term
forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax
t1 Var
x)
      UType
_ -> SrcLoc -> TypeErr -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m USyntax) -> TypeErr -> m USyntax
forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInferProj (Syntax -> Var -> Term
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 USyntax
m' <- (Var -> Maybe Syntax -> m USyntax)
-> Map Var (Maybe Syntax) -> m (Map Var USyntax)
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(Var -> a -> f b) -> Map Var a -> f (Map Var b)
itraverse (\Var
x -> Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer (Syntax -> m USyntax)
-> (Maybe Syntax -> Syntax) -> Maybe Syntax -> m USyntax
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Syntax -> Maybe Syntax -> Syntax
forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (Var -> Term
forall ty. Var -> Term' ty
TVar Var
x))) Map Var (Maybe Syntax)
m
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Map Var (Maybe USyntax) -> Term' UType
forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (USyntax -> Maybe USyntax
forall a. a -> Maybe a
Just (USyntax -> Maybe USyntax)
-> Map Var USyntax -> Map Var (Maybe USyntax)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var USyntax
m')) Comments
cs (Map Var UType -> UType
UTyRcd ((USyntax -> UType) -> Map Var USyntax -> Map Var UType
forall a b. (a -> b) -> Map Var a -> Map Var b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType) Map Var USyntax
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
    TydefInfo
_ <- SrcLoc
-> (KindError -> TypeErr)
-> ThrowC KindError m TydefInfo
-> m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l KindError -> TypeErr
KindErr (ThrowC KindError m TydefInfo -> m TydefInfo)
-> ThrowC KindError m TydefInfo -> m TydefInfo
forall a b. (a -> b) -> a -> b
$ Polytype -> ThrowC KindError m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Ctx TydefInfo)) sig m,
 Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
checkPolytypeKind Polytype
pty
    let upty :: U Polytype
upty = Polytype -> U Polytype
forall t. WithU t => t -> U t
toU Polytype
pty
    -- Typecheck against skolemized polytype.
    UType
uty <- UPolytype -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
skolemize UPolytype
upty
    USyntax
_ <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
c UType
uty
    -- Make sure no skolem variables have escaped.
    forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @UCtx m UCtx -> (UCtx -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UPolytype -> m ()) -> UCtx -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> UPolytype -> m ()
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.
    UType
iuty <- UPolytype -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
instantiate UPolytype
upty
    USyntax
c' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
c UType
iuty
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> Polytype -> Term' UType
forall ty. Syntax' ty -> Polytype -> Term' ty
SAnnotate USyntax
c' Polytype
pty) Comments
cs UType
iuty

  -- Fallback: to infer the type of anything else, make up a fresh unification
  -- variable for its type and check against it.
  Term
_ -> do
    UType
sTy <- m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh
    Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s UType
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
Volume -> [tyQ| Int -> Cmd (Unit + Int) |]
  Const
Path -> [tyQ| (Unit + Int) -> ((Int * Int) + Text) -> Cmd (Unit + (Dir * Int)) |]
  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
Sow -> [tyQ| Text -> Cmd Unit |]
  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 -> (Unit + 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
Structure -> [tyQ| Text -> Int -> Cmd (Unit + (Int * (Int * Int))) |]
  Const
Floorplan -> [tyQ| Text -> Cmd (Int * Int) |]
  Const
HasTag -> [tyQ| Text -> Text -> Cmd Bool |]
  Const
TagMembers -> [tyQ| Text -> Int -> Cmd (Int * Text) |]
  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| Cmd (rec l. Unit + Actor * l) |]
  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 ::
  ( Has (Reader UCtx) sig m
  , Has (Reader ReqCtx) sig m
  , Has (Reader TDCtx) sig m
  , Has (Reader TCStack) sig m
  , Has Unification sig m
  , Has (Error ContextualTypeErr) sig m
  ) =>
  Syntax ->
  UType ->
  m (Syntax' UType)
check :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check s :: Syntax
s@(CSyntax SrcLoc
l Term
t Comments
cs) UType
expected = SrcLoc -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Catch ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> m a -> m a
addLocToTypeErr SrcLoc
l (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ case Term
t of
  -- If t : ty, then  {t} : {ty}.
  SDelay Syntax
s1 -> do
    UType
ty1 <- Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeDelayTy Syntax
s (Source
Expected, UType
expected)
    USyntax
s1' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s1 UType
ty1
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> Term' UType
forall ty. Syntax' ty -> Term' ty
SDelay USyntax
s1') Comments
cs (UType -> UType
UTyDelay UType
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
    (UType
ty1, UType
ty2) <- Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeProdTy Syntax
s (Source
Expected, UType
expected)
    USyntax
s1' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s1 UType
ty1
    USyntax
s2' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s2 UType
ty2
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> USyntax -> Term' UType
forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SPair USyntax
s1' USyntax
s2') Comments
cs (UType -> UType -> UType
UTyProd UType
ty1 UType
ty2)

  -- To check a lambda, make sure the expected type is a function type.
  SLam LocVar
x Maybe (Fix TypeF)
mxTy Syntax
body -> do
    (UType
argTy, UType
resTy) <- Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeFunTy Syntax
s (Source
Expected, UType
expected)
    (Fix TypeF -> m ()) -> Maybe (Fix TypeF) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (SrcLoc -> (KindError -> TypeErr) -> ThrowC KindError m () -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l KindError -> TypeErr
KindErr (ThrowC KindError m () -> m ())
-> (Fix TypeF -> ThrowC KindError m ()) -> Fix TypeF -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix TypeF -> ThrowC KindError m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Ctx TydefInfo)) sig m,
 Has (Throw KindError) sig m) =>
Fix TypeF -> m ()
checkKind) Maybe (Fix TypeF)
mxTy
    case Maybe (Fix TypeF) -> U (Maybe (Fix TypeF))
forall t. WithU t => t -> U t
toU Maybe (Fix TypeF)
mxTy of
      Just UType
xTy -> do
        Either UnificationError UType
res <- UType
argTy UType -> UType -> m (Either UnificationError UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> UType -> m (Either UnificationError UType)
=:= UType
xTy
        case Either UnificationError UType
res 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.
          Left UnificationError
_ -> SrcLoc -> TypeErr -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m ()) -> TypeErr -> m ()
forall a b. (a -> b) -> a -> b
$ TypeJoin -> TypeErr
LambdaArgMismatch (UType -> UType -> TypeJoin
forall a. a -> a -> Join a
joined UType
argTy UType
xTy)
          Right UType
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe UType
U (Maybe (Fix TypeF))
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    USyntax
body' <- Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) ([Var] -> UType -> UPolytype
forall t. [Var] -> t -> Poly t
Forall [] UType
argTy) (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
body UType
resTy
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (LocVar -> Maybe (Fix TypeF) -> USyntax -> Term' UType
forall ty. LocVar -> Maybe (Fix TypeF) -> Syntax' ty -> Term' ty
SLam LocVar
x Maybe (Fix TypeF)
mxTy USyntax
body') Comments
cs (UType -> UType -> UType
UTyFun UType
argTy UType
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 Const -> [Const] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> do
        UType
argTy <- Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy Syntax
s (Source
Expected, UType
expected)
        USyntax
at' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
at (UType -> UType
UTyCmd UType
argTy)
        USyntax
atomic' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer (SrcLoc -> Term -> Syntax
Syntax SrcLoc
l (Const -> Term
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.
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
Atomic) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Syntax -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Syntax -> m ()
validAtomic Syntax
at
        USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> USyntax -> Term' UType
forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp USyntax
atomic' USyntax
at') Comments
cs (UType -> UType
UTyCmd UType
argTy)

  -- Checking the type of a let- or def-expression.
  SLet LetSyntax
ls Bool
r LocVar
x Maybe Polytype
mxTy Maybe Requirements
_ Syntax
t1 Syntax
t2 -> SrcLoc -> TCFrame -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l (Var -> TCFrame
TCLet (LocVar -> Var
lvVar LocVar
x)) (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ do
    (Polytype -> m TydefInfo) -> Maybe Polytype -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (SrcLoc
-> (KindError -> TypeErr)
-> ThrowC KindError m TydefInfo
-> m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l KindError -> TypeErr
KindErr (ThrowC KindError m TydefInfo -> m TydefInfo)
-> (Polytype -> ThrowC KindError m TydefInfo)
-> Polytype
-> m TydefInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polytype -> ThrowC KindError m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Ctx TydefInfo)) sig m,
 Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
checkPolytypeKind) Maybe Polytype
mxTy
    (UPolytype
upty, USyntax
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.
        UType
xTy <- m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
m UType
fresh
        USyntax
t1' <- Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) ([Var] -> UType -> UPolytype
forall t. [Var] -> t -> Poly t
Forall [] UType
xTy) (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
t1
        let uty :: UType
uty = USyntax
t1' USyntax -> Getting UType USyntax UType -> UType
forall s a. s -> Getting a s a -> a
^. Getting UType USyntax UType
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType
        Either UnificationError UType
_ <- UType
xTy UType -> UType -> m (Either UnificationError UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> UType -> m (Either UnificationError UType)
=:= UType
uty
        UPolytype
upty <- UType -> m UPolytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader UCtx) sig m) =>
UType -> m UPolytype
generalize UType
uty
        (UPolytype, USyntax) -> m (UPolytype, USyntax)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, USyntax
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 = Polytype -> U Polytype
forall t. WithU t => t -> U t
toU Polytype
pty
        UType
uty <- UPolytype -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UType
skolemize UPolytype
upty
        USyntax
t1' <- Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
t1 UType
uty
        (UPolytype, USyntax) -> m (UPolytype, USyntax)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, USyntax
t1')

    -- Check the requirements of t1.
    Ctx TydefInfo
tdCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TDCtx
    Ctx Requirements
reqCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @ReqCtx
    let Syntax' SrcLoc
_ Term
tt1 Comments
_ ()
_ = Syntax
t1
        reqs :: Requirements
reqs = Ctx TydefInfo -> Ctx Requirements -> Term -> Requirements
requirements Ctx TydefInfo
tdCtx Ctx Requirements
reqCtx Term
tt1

    -- If we are checking a 'def', ensure t2 has a command type.  This ensures that
    -- something like 'def ... end; x + 3' is not allowed, since this
    -- would result in the whole thing being wrapped in return, like
    -- 'return (def ... end; x + 3)', which means the def would be local and
    -- not persist to the next REPL input, which could be surprising.
    --
    -- On the other hand, 'let x = y in x + 3' is perfectly fine.
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (LetSyntax
ls LetSyntax -> LetSyntax -> Bool
forall a. Eq a => a -> a -> Bool
== LetSyntax
LSDef) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m UType -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m UType -> m ()) -> m UType -> m ()
forall a b. (a -> b) -> a -> b
$ Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy Syntax
t2 (Source
Expected, UType
expected)

    -- Now check the type of the body, under a context extended with
    -- the type and requirements of the bound variable.
    USyntax
t2' <-
      Var -> UPolytype -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$
        Var -> Requirements -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) Requirements
reqs (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$
          Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
t2 UType
expected

    -- Make sure no skolem variables have escaped.
    forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @UCtx m UCtx -> (UCtx -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UPolytype -> m ()) -> UCtx -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> UPolytype -> m ()
noSkolems SrcLoc
l)

    -- Annotate a 'def' with requirements, but not 'let'.  The reason
    -- is so that let introduces truly "local" bindings which never
    -- persist, but def introduces "global" bindings.  Variables bound
    -- in the environment can only be used to typecheck future REPL
    -- terms if the environment holds not only a value but also a type
    -- + requirements for them.  For example:
    --
    -- > def x : Int = 3 end; return (x + 2)
    -- 5
    -- > x
    -- 3
    -- > let y : Int = 3 in y + 2
    -- 5
    -- > y
    -- 1:1: Unbound variable y
    -- > let y = 3 in def x = 5 end; return (x + y)
    -- 8
    -- > y
    -- 1:1: Unbound variable y
    -- > x
    -- 5
    let mreqs :: Maybe Requirements
mreqs = case LetSyntax
ls of
          LetSyntax
LSDef -> Requirements -> Maybe Requirements
forall a. a -> Maybe a
Just Requirements
reqs
          LetSyntax
LSLet -> Maybe Requirements
forall a. Maybe a
Nothing

    -- Return the annotated let.
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (LetSyntax
-> Bool
-> LocVar
-> Maybe Polytype
-> Maybe Requirements
-> USyntax
-> USyntax
-> Term' UType
forall ty.
LetSyntax
-> Bool
-> LocVar
-> Maybe Polytype
-> Maybe Requirements
-> Syntax' ty
-> Syntax' ty
-> Term' ty
SLet LetSyntax
ls Bool
r LocVar
x Maybe Polytype
mxTy Maybe Requirements
mreqs USyntax
t1' USyntax
t2') Comments
cs UType
expected

  -- Kind-check a type definition and then check the body under an
  -- extended context.
  STydef LocVar
x Polytype
pty Maybe TydefInfo
_ Syntax
t1 -> do
    TydefInfo
tydef <- SrcLoc
-> (KindError -> TypeErr)
-> ThrowC KindError m TydefInfo
-> m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) e a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> (e -> TypeErr) -> ThrowC e m a -> m a
adaptToTypeErr SrcLoc
l KindError -> TypeErr
KindErr (ThrowC KindError m TydefInfo -> m TydefInfo)
-> ThrowC KindError m TydefInfo -> m TydefInfo
forall a b. (a -> b) -> a -> b
$ Polytype -> ThrowC KindError m TydefInfo
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Ctx TydefInfo)) sig m,
 Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
checkPolytypeKind Polytype
pty
    USyntax
t1' <- Var -> TydefInfo -> m USyntax -> m USyntax
forall t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader (Ctx t)) sig m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) TydefInfo
tydef (Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
t1 UType
expected)
    -- Eliminate the type alias in the reported type, since it is not
    -- in scope in the ambient context to which we report back the type.
    UType
expected' <- Var -> TydefInfo -> UType -> UType
forall t. Typical t => Var -> TydefInfo -> t -> t
elimTydef (LocVar -> Var
lvVar LocVar
x) TydefInfo
tydef (UType -> UType) -> m UType -> m UType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UType -> m UType
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UType -> m UType
applyBindings UType
expected
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (LocVar -> Polytype -> Maybe TydefInfo -> USyntax -> Term' UType
forall ty.
LocVar -> Polytype -> Maybe TydefInfo -> Syntax' ty -> Term' ty
STydef LocVar
x Polytype
pty (TydefInfo -> Maybe TydefInfo
forall a. a -> Maybe a
Just TydefInfo
tydef) USyntax
t1') Comments
cs UType
expected'

  -- 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 UType
tyMap <- UType
expected -> do
        let expectedFields :: Set Var
expectedFields = Map Var UType -> Set Var
forall k a. Map k a -> Set k
M.keysSet Map Var UType
tyMap
            actualFields :: Set Var
actualFields = Map Var (Maybe Syntax) -> Set Var
forall k a. Map k a -> Set k
M.keysSet Map Var (Maybe Syntax)
fields
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set Var
actualFields Set Var -> Set Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Set Var
expectedFields) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
          SrcLoc -> TypeErr -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m ()) -> TypeErr -> m ()
forall a b. (a -> b) -> a -> b
$
            Join (Set Var) -> TypeErr
FieldsMismatch (Set Var -> Set Var -> Join (Set Var)
forall a. a -> a -> Join a
joined Set Var
expectedFields Set Var
actualFields)
        Map Var USyntax
m' <- (Var -> Maybe Syntax -> m USyntax)
-> Map Var (Maybe Syntax) -> m (Map Var USyntax)
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(Var -> a -> f b) -> Map Var a -> f (Map Var b)
itraverse (\Var
x Maybe Syntax
ms -> Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check (Syntax -> Maybe Syntax -> Syntax
forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (Var -> Term
forall ty. Var -> Term' ty
TVar Var
x)) Maybe Syntax
ms) (Map Var UType
tyMap Map Var UType -> Var -> UType
forall k a. Ord k => Map k a -> k -> a
! Var
x)) Map Var (Maybe Syntax)
fields
        USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (Map Var (Maybe USyntax) -> Term' UType
forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (USyntax -> Maybe USyntax
forall a. a -> Maybe a
Just (USyntax -> Maybe USyntax)
-> Map Var USyntax -> Map Var (Maybe USyntax)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var USyntax
m')) Comments
cs UType
expected

  -- The type of @suspend t@ is @Cmd T@ if @t : T@.
  SSuspend Syntax
s1 -> do
    UType
argTy <- Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m UType
decomposeCmdTy Syntax
s (Source
Expected, UType
expected)
    USyntax
s1' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s1 UType
argTy
    USyntax -> m USyntax
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (USyntax -> m USyntax) -> USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l (USyntax -> Term' UType
forall ty. Syntax' ty -> Term' ty
SSuspend USyntax
s1') Comments
cs UType
expected

  -- Fallback: switch into inference mode, and check that the type we
  -- get is what we expected.
  Term
_ -> do
    Syntax' SrcLoc
l' Term' UType
t' Comments
_ UType
actual <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader (Ctx Requirements)) sig m,
 Has (Reader (Ctx TydefInfo)) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
s
    SrcLoc -> Term' UType -> Comments -> UType -> USyntax
forall ty. SrcLoc -> Term' ty -> Comments -> ty -> Syntax' ty
Syntax' SrcLoc
l' Term' UType
t' Comments
cs (UType -> USyntax) -> m UType -> m USyntax
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Syntax -> TypeJoin -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
Maybe Syntax -> TypeJoin -> m UType
unify (Syntax -> Maybe Syntax
forall a. a -> Maybe a
Just Syntax
s) (UType -> UType -> TypeJoin
forall a. a -> a -> Join a
joined UType
expected UType
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 ::
  ( Has (Reader UCtx) sig m
  , Has (Reader TCStack) sig m
  , Has Unification sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  Syntax ->
  m ()
validAtomic :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Syntax -> m ()
validAtomic s :: Syntax
s@(Syntax SrcLoc
l Term
t) = do
  Int
n <- Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
forall a. Set a
S.empty Syntax
s
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ SrcLoc -> TypeErr -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m ()) -> TypeErr -> m ()
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 ::
  ( Has (Reader UCtx) sig m
  , Has (Reader TCStack) sig m
  , Has Unification sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  Set Var ->
  Syntax ->
  m Int
analyzeAtomic :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m 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 {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TDir {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TInt {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TAntiInt {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TText {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TAntiText {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TBool {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRobot {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRequireDevice {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TRequire {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  SRequirements {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  STydef {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  -- Constants.
  TConst Const
c
    -- Nested 'atomic' is not allowed.
    | Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
Atomic -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
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 -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
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 -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> m Int) -> Int -> m Int
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 ->
    Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> m Int -> m (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
tst m (Int -> Int) -> m Int -> m Int
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> Int -> Int) -> m Int -> m (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
thn m (Int -> Int) -> m Int -> m Int
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
els)
  -- Pairs, application, and delay are simple: just recurse and sum the results.
  SPair Syntax
s1 Syntax
s2 -> Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> m Int -> m (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s1 m (Int -> Int) -> m Int -> m Int
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s2
  SApp Syntax
s1 Syntax
s2 -> Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> m Int -> m (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s1 m (Int -> Int) -> m Int -> m Int
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s2
  SDelay Syntax
s1 -> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m 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 Maybe ()
_ Maybe Polytype
_ Maybe Requirements
_ Syntax
s1 Syntax
s2 -> Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> m Int -> m (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s1 m (Int -> Int) -> m Int -> m Int
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic ((Set Var -> Set Var)
-> (LocVar -> Set Var -> Set Var)
-> Maybe LocVar
-> Set Var
-> Set Var
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Var -> Set Var
forall a. a -> a
id (Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
S.insert (Var -> Set Var -> Set Var)
-> (LocVar -> Var) -> LocVar -> Set Var -> Set Var
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 -> [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> m [Int] -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Var, Maybe Syntax) -> m Int) -> [(Var, Maybe Syntax)] -> m [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var, Maybe Syntax) -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
(Var, Maybe Syntax) -> m Int
analyzeField (Map Var (Maybe Syntax) -> [(Var, Maybe Syntax)]
forall k a. Map k a -> [(k, a)]
M.assocs Map Var (Maybe Syntax)
m)
   where
    analyzeField ::
      ( Has (Reader UCtx) sig m
      , Has (Reader TCStack) sig m
      , Has Unification sig m
      , Has (Throw ContextualTypeErr) sig m
      ) =>
      (Var, Maybe Syntax) ->
      m Int
    analyzeField :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
(Var, Maybe Syntax) -> m Int
analyzeField (Var
x, Maybe Syntax
Nothing) = Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals (Term -> Syntax
STerm (Var -> Term
forall ty. Var -> Term' ty
TVar Var
x))
    analyzeField (Var
_, Just Syntax
s) = Set Var -> Syntax -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s
  SProj {} -> Int -> m Int
forall a. a -> m a
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 Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Var
locals -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
    | Bool
otherwise -> do
        Maybe UPolytype
mxTy <- Var -> UCtx -> Maybe UPolytype
forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x (UCtx -> Maybe UPolytype) -> m UCtx -> m (Maybe UPolytype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @UCtx
        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 -> Int -> m Int
forall a. a -> m a
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' <- UPolytype -> m UPolytype
forall u (sig :: (* -> *) -> * -> *) (m :: * -> *).
(HasBindings u, Has Unification sig m) =>
u -> m u
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
UPolytype -> m UPolytype
applyBindings UPolytype
xTy
            if UPolytype -> Bool
isSimpleUPolytype UPolytype
xTy'
              then Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
              else SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
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 {} -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
  SLet {} -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
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 {} -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
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 -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has Unification sig m, Has (Throw ContextualTypeErr) sig m) =>
Set Var -> Syntax -> m Int
analyzeAtomic Set Var
locals Syntax
s
  -- We should never encounter a suspend since it cannot be written
  -- explicitly in the surface syntax.
  SSuspend {} -> SrcLoc -> TypeErr -> m Int
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Int) -> TypeErr -> m Int
forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicSuspend Term
t

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

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