{-# LANGUAGE DataKinds #-}
{-# 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 (..),
  prettyTypeErrText,

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

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

  -- * Typechecking monad
  fresh,

  -- * Unification
  instantiate,
  skolemize,
  generalize,

  -- * Type inference
  inferTop,
  checkTop,
  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 (view, (^.))
import Control.Lens.Indexed (itraverse)
import Control.Monad (forM, forM_, void, when, (<=<), (>=>))
import Control.Monad.Free qualified as Free
import Data.Data (Data, gmapM)
import Data.Foldable (fold)
import Data.Functor.Identity
import Data.Generics (mkM)
import Data.Map (Map, (!))
import Data.Map qualified as M
import Data.Maybe
import Data.Set (Set, (\\))
import Data.Set qualified as S
import Data.Text (Text)
import Data.Text qualified as T
import Prettyprinter
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 (..), processPolytype, processType)
import Swarm.Language.Parser.QQ (tyQ)
import Swarm.Language.Parser.Util (getLocRange)
import Swarm.Language.Requirements.Analysis (requirements)
import Swarm.Language.Requirements.Type (ReqCtx)
import Swarm.Language.Syntax
import Swarm.Language.TDVar (TDVar, tdVarName)
import Swarm.Language.Types
import Swarm.Pretty
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 an application.  Stored Syntax is the term
  --   on the RHS.
  TCAppL :: Syntax -> TCFrame
  -- | Checking the RHS of an application.  Stored Syntax is the term
  -- on the LHS.
  TCAppR :: Syntax -> 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)

instance PrettyPrec TCFrame where
  prettyPrec :: forall ann. Int -> TCFrame -> Doc ann
prettyPrec Int
_ = \case
    TCLet Var
x -> Doc ann
"While checking the definition of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x
    TCAppL Syntax
s -> Doc ann
"While checking a function applied to an argument: _" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Syntax -> Doc ann
forall ann. Int -> Syntax -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
11 Syntax
s
    TCAppR Syntax
s -> Doc ann
"While checking the argument to a function:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Syntax -> Doc ann
forall ann. Int -> Syntax -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
10 Syntax
s Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"_"

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

instance PrettyPrec LocatedTCFrame where
  prettyPrec :: forall ann. Int -> LocatedTCFrame -> Doc ann
prettyPrec Int
p (LocatedTCFrame SrcLoc
_ TCFrame
f) = Int -> TCFrame -> Doc ann
forall ann. Int -> TCFrame -> Doc ann
forall a ann. PrettyPrec a => Int -> a -> Doc ann
prettyPrec Int
p TCFrame
f

-- | 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 ->
  TVCtx ->
  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx (ReaderC TVCtx m)))))) USyntax ->
  m (Either ContextualTypeErr TSyntax)
runTC' :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Algebra sig m =>
TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
     USyntax
-> m (Either ContextualTypeErr TSyntax)
runTC' TCtx
ctx Ctx Var Requirements
reqCtx TDCtx
tdctx TVCtx
tvCtx =
  (ReaderC
  UCtx
  (ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC
              (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
  USyntax
-> (USyntax
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC
                     (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
         TSyntax)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
     TSyntax
forall a b.
ReaderC
  UCtx
  (ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC
              (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
  a
-> (a
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC
                     (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
         b)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
   USyntax
 -> ReaderC
      UCtx
      (ReaderC
         [LocatedTCFrame]
         (ErrorC
            ContextualTypeErr
            (UnificationC
               (ReaderC
                  (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
      TSyntax)
-> (ReaderC
      UCtx
      (ReaderC
         [LocatedTCFrame]
         (ErrorC
            ContextualTypeErr
            (UnificationC
               (ReaderC
                  (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
     TSyntax
-> ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC
              (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
   TSyntax
 -> ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC
               (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))))
      TSyntax)
-> (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC
               (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))))
     TSyntax
-> ErrorC
     ContextualTypeErr
     (UnificationC
        (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))
     TSyntax
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader []
    (ReaderC
   [LocatedTCFrame]
   (ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC
            (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))))
   TSyntax
 -> ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))
      TSyntax)
-> (ErrorC
      ContextualTypeErr
      (UnificationC
         (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))
      TSyntax
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     [LocatedTCFrame]
     (ErrorC
        ContextualTypeErr
        (UnificationC
           (ReaderC
              (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))
  TSyntax
-> UnificationC
     (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))
     (Either ContextualTypeErr TSyntax)
forall exc (m :: * -> *) a. ErrorC exc m a -> m (Either exc a)
runError
    (ErrorC
   ContextualTypeErr
   (UnificationC
      (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))
   TSyntax
 -> UnificationC
      (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))
      (Either ContextualTypeErr TSyntax))
-> (UnificationC
      (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))
      (Either ContextualTypeErr TSyntax)
    -> m (Either ContextualTypeErr TSyntax))
-> ErrorC
     ContextualTypeErr
     (UnificationC
        (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))
  (Either ContextualTypeErr TSyntax)
-> ReaderC
     (Ctx Var Requirements)
     (ReaderC TDCtx (ReaderC TVCtx m))
     (Either UnificationError (Either ContextualTypeErr TSyntax))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Algebra sig m, Has (Reader TDCtx) sig m) =>
UnificationC m a -> m (Either UnificationError a)
U.runUnification
    (UnificationC
   (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m)))
   (Either ContextualTypeErr TSyntax)
 -> ReaderC
      (Ctx Var Requirements)
      (ReaderC TDCtx (ReaderC TVCtx m))
      (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (ReaderC
      (Ctx Var Requirements)
      (ReaderC TDCtx (ReaderC TVCtx m))
      (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> UnificationC
     (ReaderC (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements
-> ReaderC
     (Ctx Var Requirements)
     (ReaderC TDCtx (ReaderC TVCtx m))
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> ReaderC
     TDCtx
     (ReaderC TVCtx m)
     (Either UnificationError (Either ContextualTypeErr TSyntax))
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader Ctx Var Requirements
reqCtx
    (ReaderC
   (Ctx Var Requirements)
   (ReaderC TDCtx (ReaderC TVCtx m))
   (Either UnificationError (Either ContextualTypeErr TSyntax))
 -> ReaderC
      TDCtx
      (ReaderC TVCtx m)
      (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (ReaderC
      TDCtx
      (ReaderC TVCtx m)
      (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     (Ctx Var Requirements)
     (ReaderC TDCtx (ReaderC TVCtx 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
>>> TDCtx
-> ReaderC
     TDCtx
     (ReaderC TVCtx m)
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> ReaderC
     TVCtx
     m
     (Either UnificationError (Either ContextualTypeErr TSyntax))
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader TDCtx
tdctx
    (ReaderC
   TDCtx
   (ReaderC TVCtx m)
   (Either UnificationError (Either ContextualTypeErr TSyntax))
 -> ReaderC
      TVCtx
      m
      (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (ReaderC
      TVCtx
      m
      (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     TDCtx
     (ReaderC TVCtx 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
>>> TVCtx
-> ReaderC
     TVCtx
     m
     (Either UnificationError (Either ContextualTypeErr TSyntax))
-> m (Either UnificationError (Either ContextualTypeErr TSyntax))
forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader TVCtx
tvCtx
    (ReaderC
   TVCtx
   m
   (Either UnificationError (Either ContextualTypeErr TSyntax))
 -> m (Either UnificationError (Either ContextualTypeErr TSyntax)))
-> (m (Either UnificationError (Either ContextualTypeErr TSyntax))
    -> m (Either ContextualTypeErr TSyntax))
-> ReaderC
     TVCtx
     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 ->
  TVCtx ->
  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx (ReaderC TVCtx Identity)))))) USyntax ->
  Either ContextualTypeErr TSyntax
runTC :: TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
-> Either ContextualTypeErr TSyntax
runTC TCtx
tctx Ctx Var Requirements
reqCtx TDCtx
tdctx TVCtx
tvCtx = TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
-> Identity (Either ContextualTypeErr TSyntax)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Algebra sig m =>
TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx m))))))
     USyntax
-> m (Either ContextualTypeErr TSyntax)
runTC' TCtx
tctx Ctx Var Requirements
reqCtx TDCtx
tdctx TVCtx
tvCtx (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC
               (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
   USyntax
 -> Identity (Either ContextualTypeErr TSyntax))
-> (Identity (Either ContextualTypeErr TSyntax)
    -> Either ContextualTypeErr TSyntax)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 (Reader TVCtx) 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 (Reader TVCtx) 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, Has (Reader TVCtx) sig m) =>
UPolytype -> m UType
instantiate (Var -> UCtx -> Maybe UPolytype
forall v t. Ord v => v -> Ctx v 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
  ) =>
  SrcLoc ->
  m a ->
  m a
addLocToTypeErr :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Catch ContextualTypeErr) 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]
stk TypeErr
te -> 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
CTE SrcLoc
l [LocatedTCFrame]
stk TypeErr
te
    ContextualTypeErr
cte -> ContextualTypeErr -> m a
forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError ContextualTypeErr
cte

------------------------------------------------------------
-- 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 q t) where
  freeUVars :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has Unification sig m =>
Poly q t -> m (Set IntVar)
freeUVars = 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 -> m (Set IntVar))
-> (Poly q t -> t) -> Poly q t -> m (Set IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly q t -> t
forall (q :: ImplicitQuantification) t. Poly q t -> t
ptBody

-- | 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 v t. Ctx v t -> Map v 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
Free.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
Free.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
o Var
v -> UType -> Maybe UType -> UType
forall a. a -> Maybe a -> a
fromMaybe (Var -> Var -> UType
UTyVar' Var
o 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.Free TypeF UType
f
    )

-- | Make sure none of the given skolem variables have escaped.
noSkolems ::
  ( Has Unification sig m
  , Has (Reader TCStack) sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  SrcLoc ->
  [Var] ->
  UPolytype ->
  m ()
noSkolems :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> [Var] -> UPolytype -> m ()
noSkolems SrcLoc
l [Var]
skolems (UPolytype -> ([Var], UType)
forall t. Poly 'Quantified t -> ([Var], t)
unPoly -> ([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
_ 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'
      freeTyvs :: Set Var
freeTyvs = 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
      escapees :: Set Var
escapees = Set Var
freeTyvs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
skolems

  -- In case of multiple escapees, just generate an error for one
  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
escapees) ((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)
U.=:= 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 = (UType -> m UType) -> UPolytype -> m UPolytype
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) -> Poly 'Quantified a -> f (Poly 'Quantified b)
traverse 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

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 Var a -> m (Ctx Var 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, Has (Reader TVCtx) sig m) => UPolytype -> m UType
instantiate :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader TVCtx) sig m) =>
UPolytype -> m UType
instantiate (UPolytype -> ([Var], UType)
forall t. Poly 'Quantified t -> ([Var], t)
unPoly -> ([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
  TVCtx
boundSubst <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TVCtx
  let s :: Map (Either Var IntVar) UType
s = (Var -> Either Var IntVar)
-> Map Var UType -> Map (Either Var IntVar) UType
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys Var -> Either Var IntVar
forall a b. a -> Either a b
Left ([(Var, UType)] -> Map Var UType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [UType] -> [(Var, UType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [UType]
xs') Map Var UType -> Map Var UType -> Map Var UType
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TVCtx -> Map Var UType
forall v t. Ctx v t -> Map v t
unCtx TVCtx
boundSubst)
  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 Map (Either Var IntVar) UType
s 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.
--
--   Returns a context mapping from instantiated type variables to generated
--   Skolem variables, along with the substituted type.
skolemize :: (Has Unification sig m, Has (Reader TVCtx) sig m) => UPolytype -> m (Ctx Var UType, UType)
skolemize :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader TVCtx) sig m) =>
UPolytype -> m (TVCtx, UType)
skolemize (UPolytype -> ([Var], UType)
forall t. Poly 'Quantified t -> ([Var], t)
unPoly -> ([Var]
xs, UType
uty)) = do
  [(Var, Var)]
skolemNames <- [Var] -> (Var -> m (Var, Var)) -> m [(Var, Var)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
xs ((Var -> m (Var, Var)) -> m [(Var, Var)])
-> (Var -> m (Var, Var)) -> m [(Var, Var)]
forall a b. (a -> b) -> a -> b
$ \Var
x -> do
    Var
s <- Var -> IntVar -> Var
mkVarName Var
"s" (IntVar -> Var) -> m IntVar -> m Var
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
    (Var, Var) -> m (Var, Var)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var
x, Var
s)
  TVCtx
boundSubst <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TVCtx
  let xs' :: [UType]
xs' = ((Var, Var) -> UType) -> [(Var, Var)] -> [UType]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> Var -> UType) -> (Var, Var) -> UType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> Var -> UType
UTyVar') [(Var, Var)]
skolemNames
      newSubst :: Map Var UType
newSubst = [(Var, UType)] -> Map Var UType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Var, UType)] -> Map Var UType)
-> [(Var, UType)] -> Map Var UType
forall a b. (a -> b) -> a -> b
$ [Var] -> [UType] -> [(Var, UType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [UType]
xs'
      s :: Map (Either Var IntVar) UType
s = (Var -> Either Var IntVar)
-> Map Var UType -> Map (Either Var IntVar) UType
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys Var -> Either Var IntVar
forall a b. a -> Either a b
Left (Map Var UType
newSubst Map Var UType -> Map Var UType -> Map Var UType
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TVCtx -> Map Var UType
forall v t. Ctx v t -> Map v t
unCtx TVCtx
boundSubst)
  (TVCtx, UType) -> m (TVCtx, UType)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Var UType -> TVCtx
forall v t. (Ord v, Hashable v, Hashable t) => Map v t -> Ctx v t
Ctx.fromMap Map Var UType
newSubst, Map (Either Var IntVar) UType -> UType -> UType
substU Map (Either Var IntVar) UType
s UType
uty)

-- | '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)
-> (Poly 'Unquantified UType -> UPolytype)
-> Poly 'Unquantified UType
-> m UPolytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly 'Unquantified UType -> UPolytype
forall t. Typical t => Poly 'Unquantified t -> Poly 'Quantified t
absQuantify (Poly 'Unquantified UType -> m UPolytype)
-> Poly 'Unquantified UType -> m UPolytype
forall a b. (a -> b) -> a -> b
$
    [Var] -> UType -> Poly 'Unquantified UType
forall t. [Var] -> t -> Poly 'Unquantified t
mkPoly
      (((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
------------------------------------------------------------

--------------------------------------------------
-- Basic type errors

-- | 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
  | -- | An undefined type was encountered.
    UnboundType TDVar
  | -- | A kind error was encountered.
    KindErr KindError
  | -- | A Skolem variable escaped its local context.
    EscapedSkolem Var
  | -- | Failure during unification.
    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
  | -- | Record type mismatch.  The given term was expected to have a
    --   record type, but has a different type instead.
    MismatchRcd (Maybe Syntax) UType
  | -- | 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
  | -- | Read must be given a literal type as an argument.  See
    --   https://github.com/swarm-game/swarm/pull/2461#discussion_r2124125021
    ReadNonLiteralTypeArg Term
  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)

instance PrettyPrec TypeErr where
  prettyPrec :: forall ann. Int -> TypeErr -> Doc ann
prettyPrec Int
_ = \case
    UnificationErr UnificationError
ue -> UnificationError -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UnificationError
ue
    KindErr KindError
ke -> KindError -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr KindError
ke
    Mismatch Maybe Syntax
Nothing (TypeJoin -> (UType, UType)
forall a. Join a -> (a, a)
getJoin -> (UType
ty1, UType
ty2)) ->
      Doc ann
"Type mismatch: expected" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
ty1 Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
", but got" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
ty2
    Mismatch (Just Syntax
t) (TypeJoin -> (UType, UType)
forall a. Join a -> (a, a)
getJoin -> (UType
ty1, UType
ty2)) ->
      Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
        [ Doc ann
"Type mismatch:"
        , Doc ann
"From context, expected" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Syntax -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Syntax
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"to" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Source -> UType -> Doc ann
forall a. Source -> UType -> Doc a
typeDescription Source
Expected UType
ty1 Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
","
        , Doc ann
"but it" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Source -> UType -> Doc ann
forall a. Source -> UType -> Doc a
typeDescription Source
Actual UType
ty2
        ]
    MismatchRcd Maybe Syntax
Nothing UType
ty ->
      Doc ann
"Type mismatch: expected a record type, but got" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
ty
    MismatchRcd (Just Syntax
t) UType
ty ->
      Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
        [ Doc ann
"Type mismatch:"
        , Doc ann
"From context, expected" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Syntax -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Syntax
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"to have a record type,"
        , Doc ann
"but it" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Source -> UType -> Doc ann
forall a. Source -> UType -> Doc a
typeDescription Source
Actual UType
ty
        ]
    LambdaArgMismatch (TypeJoin -> (UType, UType)
forall a. Join a -> (a, a)
getJoin -> (UType
ty1, UType
ty2)) ->
      Doc ann
"Lambda argument has type annotation" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode UType
ty2 Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
", but expected argument type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> UType -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode UType
ty1
    FieldsMismatch (Join (Set Var) -> (Set Var, Set Var)
forall a. Join a -> (a, a)
getJoin -> (Set Var
expFs, Set Var
actFs)) ->
      Set Var -> Set Var -> Doc ann
forall a. Set Var -> Set Var -> Doc a
fieldMismatchMsg Set Var
expFs Set Var
actFs
    EscapedSkolem Var
x ->
      Doc ann
"Skolem variable" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"would escape its scope"
    UnboundVar Var
x ->
      Doc ann
"Unbound variable" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x
    UnboundType TDVar
x ->
      Doc ann
"Undefined type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TDVar -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TDVar
x
    DefNotTopLevel Term
t ->
      Doc ann
"Definitions may only be at the top level:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t
    CantInfer Term
t ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
        [ Doc ann
"Couldn't infer the type of term:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t
        , Doc ann
forall ann. Doc ann
reportBug
        ]
    CantInferProj Term
t ->
      Doc ann
"In the record projection" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
", can't infer whether the LHS has a record type.  Try adding a type annotation."
    UnknownProj Var
x Term
t ->
      Doc ann
"Record does not have a field with name" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t
    InvalidAtomic InvalidAtomicReason
reason Term
t ->
      Doc ann
"Invalid atomic block:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> InvalidAtomicReason -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr InvalidAtomicReason
reason Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t
    TypeErr
Impredicative ->
      Doc ann
"Unconstrained unification type variables encountered, likely due to an impredicative type. This is a known bug; for more information see https://github.com/swarm-game/swarm/issues/351 ."
    ReadNonLiteralTypeArg Term
t ->
      Doc ann
"The `read` command must be given a literal type as its first argument (Swarm does not have dependent types); found" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
pprCode Term
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"instead."
   where
    pprCode :: PrettyPrec a => a -> Doc ann
    pprCode :: forall a ann. PrettyPrec a => a -> Doc ann
pprCode = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
bquote (Doc ann -> Doc ann) -> (a -> Doc ann) -> a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr

-- | Given a type and its source, construct an appropriate description
--   of it to go in a type mismatch error message.
typeDescription :: Source -> UType -> Doc a
typeDescription :: forall a. Source -> UType -> Doc a
typeDescription Source
src UType
ty
  | Bool -> Bool
not (UType -> Bool
hasAnyUVars UType
ty) =
      Source -> Doc a -> Doc a -> Doc a
forall a. Source -> a -> a -> a
withSource Source
src Doc a
"have" Doc a
"actually has" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"type" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a -> Doc a
forall ann. Doc ann -> Doc ann
bquote (UType -> Doc a
forall a ann. PrettyPrec a => a -> Doc ann
ppr UType
ty)
  | Just TypeF ()
f <- UType -> Maybe (TypeF ())
isTopLevelConstructor UType
ty =
      Source -> Doc a -> Doc a -> Doc a
forall a. Source -> a -> a -> a
withSource Source
src Doc a
"be" Doc a
"is actually" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeF () -> Doc a
forall a. TypeF () -> Doc a
tyNounPhrase TypeF ()
f
  | Bool
otherwise =
      Source -> Doc a -> Doc a -> Doc a
forall a. Source -> a -> a -> a
withSource Source
src Doc a
"have" Doc a
"actually has" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"a type like" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a -> Doc a
forall ann. Doc ann -> Doc ann
bquote (Free TypeF Wildcard -> Doc a
forall a ann. PrettyPrec a => a -> Doc ann
ppr ((IntVar -> Wildcard) -> UType -> Free TypeF Wildcard
forall a b. (a -> b) -> Free TypeF a -> Free TypeF b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Wildcard -> IntVar -> Wildcard
forall a b. a -> b -> a
const Wildcard
Wildcard) UType
ty))

-- | Return an English noun phrase describing things with the given
--   top-level type constructor.
tyNounPhrase :: TypeF () -> Doc a
tyNounPhrase :: forall a. TypeF () -> Doc a
tyNounPhrase = \case
  TyConF TyCon
c [()]
_ -> TyCon -> Doc a
forall a. TyCon -> Doc a
tyConNounPhrase TyCon
c
  TyVarF {} -> Doc a
"a type variable"
  TyRcdF {} -> Doc a
"a record"
  TyRecF {} -> Doc a
"a recursive type"
  TyRecVarF {} -> Doc a
"a recursive type variable"

tyConNounPhrase :: TyCon -> Doc a
tyConNounPhrase :: forall a. TyCon -> Doc a
tyConNounPhrase = \case
  TCBase BaseTy
b -> BaseTy -> Doc a
forall a. BaseTy -> Doc a
baseTyNounPhrase BaseTy
b
  TyCon
TCCmd -> Doc a
"a command"
  TyCon
TCDelay -> Doc a
"a delayed expression"
  TyCon
TCSum -> Doc a
"a sum"
  TyCon
TCProd -> Doc a
"a pair"
  TyCon
TCFun -> Doc a
"a function"
  TCUser TDVar
t -> TDVar -> Doc a
forall a ann. PrettyPrec a => a -> Doc ann
ppr TDVar
t

-- | Return an English noun phrase describing things with the given
--   base type.
baseTyNounPhrase :: BaseTy -> Doc a
baseTyNounPhrase :: forall a. BaseTy -> Doc a
baseTyNounPhrase = \case
  BaseTy
BVoid -> Doc a
"void"
  BaseTy
BUnit -> Doc a
"the unit value"
  BaseTy
BInt -> Doc a
"an integer"
  BaseTy
BText -> Doc a
"text"
  BaseTy
BDir -> Doc a
"a direction"
  BaseTy
BBool -> Doc a
"a boolean"
  BaseTy
BActor -> Doc a
"an actor"
  BaseTy
BKey -> Doc a
"a key"
  BaseTy
BType -> Doc a
"a type"

-- | Generate an appropriate message when the sets of fields in two
--   record types do not match, explaining which fields are extra and
--   which are missing.
fieldMismatchMsg :: Set Var -> Set Var -> Doc a
fieldMismatchMsg :: forall a. Set Var -> Set Var -> Doc a
fieldMismatchMsg Set Var
expFs Set Var
actFs =
  Int -> Doc a -> Doc a
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc a -> Doc a) -> ([Doc a] -> Doc a) -> [Doc a] -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vcat ([Doc a] -> Doc a) -> [Doc a] -> Doc a
forall a b. (a -> b) -> a -> b
$
    [Doc a
"Field mismatch; record literal has:"]
      [Doc a] -> [Doc a] -> [Doc a]
forall a. [a] -> [a] -> [a]
++ [Doc a
"- Extra field(s)" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Set Var -> Doc a
forall {ann}. Set Var -> Doc ann
prettyFieldSet Set Var
extraFs | Bool -> Bool
not (Set Var -> Bool
forall a. Set a -> Bool
S.null Set Var
extraFs)]
      [Doc a] -> [Doc a] -> [Doc a]
forall a. [a] -> [a] -> [a]
++ [Doc a
"- Missing field(s)" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Set Var -> Doc a
forall {ann}. Set Var -> Doc ann
prettyFieldSet Set Var
missingFs | Bool -> Bool
not (Set Var -> Bool
forall a. Set a -> Bool
S.null Set Var
missingFs)]
 where
  extraFs :: Set Var
extraFs = Set Var
actFs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Var
expFs
  missingFs :: Set Var
missingFs = Set Var
expFs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Set Var
actFs
  prettyFieldSet :: Set Var -> Doc ann
prettyFieldSet = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann)
-> (Set Var -> [Doc ann]) -> Set Var -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," ([Doc ann] -> [Doc ann])
-> (Set Var -> [Doc ann]) -> Set Var -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Doc ann) -> [Var] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
bquote (Doc ann -> Doc ann) -> (Var -> Doc ann) -> Var -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr) ([Var] -> [Doc ann]) -> (Set Var -> [Var]) -> Set Var -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Var -> [Var]
forall a. Set a -> [a]
S.toList

--------------------------------------------------
-- Errors for 'atomic'

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

instance PrettyPrec InvalidAtomicReason where
  prettyPrec :: forall ann. Int -> InvalidAtomicReason -> Doc ann
prettyPrec Int
_ = \case
    TooManyTicks Int
n -> Doc ann
"block could take too many ticks (" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"
    InvalidAtomicReason
AtomicDupingThing -> Doc ann
"def, let, and lambda are not allowed"
    NonSimpleVarType Var
_ UPolytype
ty ->
      Doc ann
"reference to variable with non-simple type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (UPolytype -> Var
forall a. PrettyPrec a => a -> Var
prettyTextLine UPolytype
ty)
    InvalidAtomicReason
NestedAtomic -> Doc ann
"nested atomic block"
    InvalidAtomicReason
LongConst -> Doc ann
"commands that can take multiple ticks to execute are not allowed"
    InvalidAtomicReason
AtomicSuspend ->
      Doc ann
"encountered a suspend command inside an atomic block" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
reportBug

--------------------------------------------------
-- Type errors with context

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

--------------------------------------------------
-- Pretty-printing for contextual type errors

-- | Format a 'ContextualTypeError' for the user and render it as
--   @Text@.
prettyTypeErrText :: Text -> ContextualTypeErr -> Text
prettyTypeErrText :: Var -> ContextualTypeErr -> Var
prettyTypeErrText Var
code = Doc Any -> Var
forall a. Doc a -> Var
docToText (Doc Any -> Var)
-> (ContextualTypeErr -> Doc Any) -> ContextualTypeErr -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> ContextualTypeErr -> Doc Any
forall ann. Var -> ContextualTypeErr -> Doc ann
prettyTypeErr Var
code

-- | Format a 'ContextualTypeError' for the user.
prettyTypeErr :: Text -> ContextualTypeErr -> Doc ann
prettyTypeErr :: forall ann. Var -> ContextualTypeErr -> Doc ann
prettyTypeErr Var
code (CTE SrcLoc
l [LocatedTCFrame]
tcStack TypeErr
te) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
    [ Doc ann
forall ann. Doc ann
teLoc Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> TypeErr -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr TypeErr
te
    , BulletList LocatedTCFrame -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr ((forall ann. Doc ann)
-> [LocatedTCFrame] -> BulletList LocatedTCFrame
forall i. (forall ann. Doc ann) -> [i] -> BulletList i
BulletList Doc a
forall ann. Doc ann
"" ([LocatedTCFrame] -> [LocatedTCFrame]
filterTCStack [LocatedTCFrame]
tcStack))
    ]
 where
  teLoc :: Doc ann
teLoc = case SrcLoc
l of
    SrcLoc Int
s Int
e -> ((Int, Int) -> Doc ann
forall {a} {a} {ann}. (Pretty a, Pretty a) => (a, a) -> Doc ann
showLoc ((Int, Int) -> Doc ann)
-> (((Int, Int), (Int, Int)) -> (Int, Int))
-> ((Int, Int), (Int, Int))
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int), (Int, Int)) -> (Int, Int)
forall a b. (a, b) -> a
fst (((Int, Int), (Int, Int)) -> Doc ann)
-> ((Int, Int), (Int, Int)) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Var -> (Int, Int) -> ((Int, Int), (Int, Int))
getLocRange Var
code (Int
s, Int
e)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
": "
    SrcLoc
NoLoc -> Doc ann
forall ann. Doc ann
emptyDoc
  showLoc :: (a, a) -> Doc ann
showLoc (a
r, a
c) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
r Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
c

-- | Filter the TCStack so we stop printing context outside of a def/let
filterTCStack :: TCStack -> TCStack
filterTCStack :: [LocatedTCFrame] -> [LocatedTCFrame]
filterTCStack [LocatedTCFrame]
tcStack = case [LocatedTCFrame]
tcStack of
  [] -> []
  -- A def/let is enough context to locate something; don't keep
  -- printing wider context after that
  t :: LocatedTCFrame
t@(LocatedTCFrame SrcLoc
_ (TCLet Var
_)) : [LocatedTCFrame]
_ -> [LocatedTCFrame
t]
  LocatedTCFrame
t : [LocatedTCFrame]
xs -> LocatedTCFrame
t LocatedTCFrame -> [LocatedTCFrame] -> [LocatedTCFrame]
forall a. a -> [a] -> [a]
: [LocatedTCFrame] -> [LocatedTCFrame]
filterTCStack [LocatedTCFrame]
xs

------------------------------------------------------------
-- 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 TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
c Syntax
t (Source
src, UTyConApp (TCUser TDVar
u) [UType]
as) = do
  UType
ty2 <- SrcLoc
-> (ExpandTydefErr -> TypeErr)
-> ThrowC ExpandTydefErr m UType
-> m UType
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
NoLoc (TDVar -> TypeErr
UnboundType (TDVar -> TypeErr)
-> (ExpandTydefErr -> TDVar) -> ExpandTydefErr -> TypeErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExpandTydefErr -> TDVar
getUnexpanded) (ThrowC ExpandTydefErr m UType -> m UType)
-> ThrowC ExpandTydefErr m UType -> m UType
forall a b. (a -> b) -> a -> b
$ TDVar -> [UType] -> ThrowC ExpandTydefErr m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [UType]
as
  TyCon -> Syntax -> Sourced UType -> m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader TDCtx) 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 TDCtx) 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 TDCtx) 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 TDCtx) 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 TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m UType
decomposeTyConApp1 TyCon
TCDelay

-- | Decompose a type which is expected to be a record type.  There
--   are three possible outcomes:
--
--     * If the type is definitely a record type, return its mapping
--       from field names to types.
--
--     * If the type is definitely not a record type, throw a type error.
--
--     * Otherwise, return @Nothing@.
--
--   This is the best we can do, and different than the way the other
--   @decompose...Ty@ functions work, because we can't solve for record
--   types via unification.
decomposeRcdTy ::
  ( Has (Reader TDCtx) sig m
  , Has (Reader TCStack) sig m
  , Has (Throw ContextualTypeErr) sig m
  ) =>
  Maybe Syntax ->
  UType ->
  m (Maybe (Map Var UType))
decomposeRcdTy :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
Maybe Syntax -> UType -> m (Maybe (Map Var UType))
decomposeRcdTy Maybe Syntax
ms = \case
  ty :: UType
ty@(UTyConApp TyCon
tc [UType]
as) -> case TyCon
tc of
    -- User-defined type: expand it
    TCUser TDVar
u -> do
      UType
ty2 <- SrcLoc
-> (ExpandTydefErr -> TypeErr)
-> ThrowC ExpandTydefErr m UType
-> m UType
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
NoLoc (TDVar -> TypeErr
UnboundType (TDVar -> TypeErr)
-> (ExpandTydefErr -> TDVar) -> ExpandTydefErr -> TypeErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExpandTydefErr -> TDVar
getUnexpanded) (ThrowC ExpandTydefErr m UType -> m UType)
-> ThrowC ExpandTydefErr m UType -> m UType
forall a b. (a -> b) -> a -> b
$ TDVar -> [UType] -> ThrowC ExpandTydefErr m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [UType]
as
      Maybe Syntax -> UType -> m (Maybe (Map Var UType))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
Maybe Syntax -> UType -> m (Maybe (Map Var UType))
decomposeRcdTy Maybe Syntax
ms UType
ty2
    -- Any other type constructor application is definitely not a record type
    TyCon
_ -> SrcLoc -> TypeErr -> m (Maybe (Map Var UType))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr (SrcLoc -> (Syntax -> SrcLoc) -> Maybe Syntax -> SrcLoc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SrcLoc
NoLoc (Getting SrcLoc Syntax SrcLoc -> Syntax -> SrcLoc
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SrcLoc Syntax SrcLoc
forall ty (f :: * -> *).
Functor f =>
(SrcLoc -> f SrcLoc) -> Syntax' ty -> f (Syntax' ty)
sLoc) Maybe Syntax
ms) (TypeErr -> m (Maybe (Map Var UType)))
-> TypeErr -> m (Maybe (Map Var UType))
forall a b. (a -> b) -> a -> b
$ Maybe Syntax -> UType -> TypeErr
MismatchRcd Maybe Syntax
ms UType
ty
  -- Recursive type: expand it
  UTyRec Var
x UType
t -> Maybe Syntax -> UType -> m (Maybe (Map Var UType))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
Maybe Syntax -> UType -> m (Maybe (Map Var UType))
decomposeRcdTy Maybe Syntax
ms (Var -> UType -> UType
forall t. SubstRec t => Var -> t -> t
unfoldRec Var
x UType
t)
  -- Record type
  UTyRcd Map Var UType
m -> Maybe (Map Var UType) -> m (Maybe (Map Var UType))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Var UType -> Maybe (Map Var UType)
forall a. a -> Maybe a
Just Map Var UType
m)
  -- With anything else (type variables, etc.) we're not sure
  UType
_ -> Maybe (Map Var UType) -> m (Maybe (Map Var UType))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Map Var UType)
forall a. Maybe a
Nothing

-- | 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 TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m) =>
TyCon -> Syntax -> Sourced UType -> m (UType, UType)
decomposeTyConApp2 TyCon
c Syntax
t (Source
src, UTyConApp (TCUser TDVar
u) [UType]
as) = do
  UType
ty2 <- SrcLoc
-> (ExpandTydefErr -> TypeErr)
-> ThrowC ExpandTydefErr m UType
-> m UType
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
NoLoc (TDVar -> TypeErr
UnboundType (TDVar -> TypeErr)
-> (ExpandTydefErr -> TDVar) -> ExpandTydefErr -> TypeErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExpandTydefErr -> TDVar
getUnexpanded) (ThrowC ExpandTydefErr m UType -> m UType)
-> ThrowC ExpandTydefErr m UType -> m UType
forall a b. (a -> b) -> a -> b
$ TDVar -> [UType] -> ThrowC ExpandTydefErr m UType
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t) =>
TDVar -> [t] -> m t
expandTydef TDVar
u [UType]
as
  TyCon -> Syntax -> Sourced UType -> m (UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Throw ContextualTypeErr) sig m,
 Has (Reader TDCtx) 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 TDCtx) 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 TDCtx) 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 TDCtx) 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 TDCtx) 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 Var Requirements
-> TDCtx
-> Syntax
-> Either ContextualTypeErr TSyntax
inferTop TCtx
ctx Ctx Var Requirements
reqCtx TDCtx
tdCtx = TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
-> Either ContextualTypeErr TSyntax
runTC TCtx
ctx Ctx Var Requirements
reqCtx TDCtx
tdCtx TVCtx
forall v t. Ctx v t
Ctx.empty (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC
               (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
   USyntax
 -> Either ContextualTypeErr TSyntax)
-> (Syntax
    -> ReaderC
         UCtx
         (ReaderC
            [LocatedTCFrame]
            (ErrorC
               ContextualTypeErr
               (UnificationC
                  (ReaderC
                     (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx 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 Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer

-- | Top level type checking function.
checkTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Type -> Either ContextualTypeErr TSyntax
checkTop :: TCtx
-> Ctx Var Requirements
-> TDCtx
-> Syntax
-> Type
-> Either ContextualTypeErr TSyntax
checkTop TCtx
ctx Ctx Var Requirements
reqCtx TDCtx
tdCtx Syntax
t Type
ty = TCtx
-> Ctx Var Requirements
-> TDCtx
-> TVCtx
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
-> Either ContextualTypeErr TSyntax
runTC TCtx
ctx Ctx Var Requirements
reqCtx TDCtx
tdCtx TVCtx
forall v t. Ctx v t
Ctx.empty (ReaderC
   UCtx
   (ReaderC
      [LocatedTCFrame]
      (ErrorC
         ContextualTypeErr
         (UnificationC
            (ReaderC
               (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
   USyntax
 -> Either ContextualTypeErr TSyntax)
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
-> Either ContextualTypeErr TSyntax
forall a b. (a -> b) -> a -> b
$ Syntax
-> UType
-> ReaderC
     UCtx
     (ReaderC
        [LocatedTCFrame]
        (ErrorC
           ContextualTypeErr
           (UnificationC
              (ReaderC
                 (Ctx Var Requirements) (ReaderC TDCtx (ReaderC TVCtx Identity))))))
     USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
t (Type -> U Type
forall t. WithU t => t -> U t
toU Type
ty)

-- | 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 processType 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 TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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) =>
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, Has (Reader TVCtx) 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
  TRequire 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
TRequire Var
d) Comments
cs (UType -> UType
UTyCmd UType
UTyUnit)
  TStock 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
TStock 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 (Reader TVCtx) 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 Type
argTy) Syntax
body -> do
    Type
argTy' <- SrcLoc
-> (KindError -> TypeErr) -> ThrowC KindError m Type -> m Type
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 Type -> m Type)
-> ThrowC KindError m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> ThrowC KindError m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) =>
Type -> m Type
processType Type
argTy
    let uargTy :: U Type
uargTy = Type -> U Type
forall t. WithU t => t -> U t
toU Type
argTy'
    USyntax
body' <- forall v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding @Var @UPolytype (LocVar -> Var
forall v. Located v -> v
lvVar LocVar
x) (UType -> UPolytype
forall t (q :: ImplicitQuantification). t -> Poly q t
mkTrivPoly 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Type -> USyntax -> Term' UType
forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check Syntax
s
  -- Special case for applying 'read' to a type argument, since we need to make
  -- sure the type propagates to the inferred output type of 'read'.
  TConst Const
Read :$: STerm Term
arg -> do
    Type
argTy <- case Term
arg of
      TType Type
ty -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
      Term
_ -> SrcLoc -> TypeErr -> m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Throw ContextualTypeErr) sig m,
 Has (Reader [LocatedTCFrame]) sig m) =>
SrcLoc -> TypeErr -> m a
throwTypeErr SrcLoc
l (TypeErr -> m Type) -> TypeErr -> m Type
forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
ReadNonLiteralTypeArg Term
arg
    USyntax
r' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer (Syntax -> m USyntax) -> Syntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ SrcLoc -> Term -> Syntax
Syntax SrcLoc
l (Const -> Term
forall ty. Const -> Term' ty
TConst Const
Read)
    Type
argTy' <- SrcLoc
-> (ExpandTydefErr -> TypeErr)
-> ThrowC ExpandTydefErr m Type
-> m Type
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 (TDVar -> TypeErr
UnboundType (TDVar -> TypeErr)
-> (ExpandTydefErr -> TDVar) -> ExpandTydefErr -> TypeErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExpandTydefErr -> TDVar
getUnexpanded) (ThrowC ExpandTydefErr m Type -> m Type)
-> ThrowC ExpandTydefErr m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> ThrowC ExpandTydefErr m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) t.
(Has (Reader TDCtx) sig m, Has (Throw ExpandTydefErr) sig m,
 Typical t, Plated t) =>
t -> m t
expandTydefs Type
argTy
    USyntax
arg' <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> UType -> m USyntax
check (Term -> Syntax
STerm (Type -> Term
forall ty. Type -> Term' ty
TType Type
argTy')) UType
UTyType
    USyntax -> m USyntax
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
r' USyntax
arg') Comments
cs (UType -> UType -> UType
UTyFun UType
UTyText (Type -> U Type
forall t. WithU t => t -> U t
toU Type
argTy'))

  -- 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', UType
argTy, UType
resTy) <- SrcLoc
-> TCFrame
-> m (USyntax, UType, UType)
-> m (USyntax, UType, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l (Syntax -> TCFrame
TCAppL Syntax
x) (m (USyntax, UType, UType) -> m (USyntax, UType, UType))
-> m (USyntax, UType, UType) -> m (USyntax, UType, UType)
forall a b. (a -> b) -> a -> b
$ do
      USyntax
f' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 TDCtx) 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)
      (USyntax, UType, UType) -> m (USyntax, UType, UType)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (USyntax
f', UType
argTy, UType
resTy)

    -- Then check that the argument has the right type.
    USyntax
x' <- SrcLoc -> TCFrame -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader [LocatedTCFrame]) sig m =>
SrcLoc -> TCFrame -> m a -> m a
withFrame SrcLoc
l (Syntax -> TCFrame
TCAppR Syntax
f) (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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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' <- Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 TDCtx) 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 v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> 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
forall v. Located v -> v
lvVar) Maybe LocVar
mx (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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 TDCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
t1
    Maybe (Map Var UType)
mm <- Maybe Syntax -> UType -> m (Maybe (Map Var UType))
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
Maybe Syntax -> UType -> m (Maybe (Map Var UType))
decomposeRcdTy (Syntax -> Maybe Syntax
forall a. a -> Maybe a
Just Syntax
t1) (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)
    case Maybe (Map Var UType)
mm of
      Just 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)
      Maybe (Map Var 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
$ 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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'))

  -- Once we're typechecking, we don't need to keep around explicit
  -- parens any more
  SParens Syntax
t1 -> Syntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) sig m,
 Has (Reader [LocatedTCFrame]) sig m, Has Unification sig m,
 Has (Error ContextualTypeErr) sig m) =>
Syntax -> m USyntax
infer Syntax
t1
  -- 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 RawPolytype
pty -> do
    Polytype
qpty <- RawPolytype -> m Polytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty.
(Has (Reader TVCtx) sig m, Typical ty) =>
Poly 'Unquantified ty -> m (Poly 'Quantified ty)
quantify RawPolytype
pty
    TydefInfo Polytype
qpty' Arity
_ <- 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 TDCtx) sig m, Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
processPolytype Polytype
qpty
    let upty :: U Polytype
upty = Polytype -> U Polytype
forall t. WithU t => t -> U t
toU Polytype
qpty'
    -- Typecheck against skolemized polytype.
    (TVCtx
skolemSubst, UType
uty) <- UPolytype -> m (TVCtx, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader TVCtx) sig m) =>
UPolytype -> m (TVCtx, UType)
skolemize UPolytype
upty
    USyntax
_ <- Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 -> [Var] -> UPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> [Var] -> UPolytype -> m ()
noSkolems SrcLoc
l (TVCtx -> [Var]
forall v t. Ctx v t -> [v]
Ctx.vars TVCtx
skolemSubst))
    -- 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, Has (Reader TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 -> RawPolytype -> Term' UType
forall ty. Syntax' ty -> RawPolytype -> Term' ty
SAnnotate USyntax
c' (Polytype -> RawPolytype
forall t. Poly 'Quantified t -> Poly 'Unquantified t
forgetQ Polytype
qpty')) Comments
cs UType
iuty
  TType Type
ty -> USyntax -> m USyntax
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 (Type -> Term' UType
forall ty. Type -> Term' ty
TType Type
ty) Comments
cs UType
UTyType
  -- 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 = Identity Polytype -> Polytype
forall a. Identity a -> a
run (Identity Polytype -> Polytype)
-> (RawPolytype -> Identity Polytype) -> RawPolytype -> Polytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r (m :: * -> *) a. r -> ReaderC r m a -> m a
runReader @TVCtx TVCtx
forall v t. Ctx v t
Ctx.empty (ReaderC TVCtx Identity Polytype -> Identity Polytype)
-> (RawPolytype -> ReaderC TVCtx Identity Polytype)
-> RawPolytype
-> Identity Polytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawPolytype -> ReaderC TVCtx Identity Polytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty.
(Has (Reader TVCtx) sig m, Typical ty) =>
Poly 'Unquantified ty -> m (Poly 'Quantified ty)
quantify (RawPolytype -> Polytype) -> RawPolytype -> Polytype
forall a b. (a -> b) -> a -> b
$ 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
LocateMe -> [tyQ| Cmd (Text * (Int * Int)) |]
  Const
Waypoints -> [tyQ| Text -> (rec l. Unit + (Int * Int) * l) |]
  Const
Structures -> [tyQ| Text -> Cmd (rec l. Unit + (Int * Int) * l) |]
  Const
Floorplan -> [tyQ| Text -> Cmd (Int * Int) |]
  Const
HasTag -> [tyQ| Text -> Text -> Bool |]
  Const
TagMembers -> [tyQ| Text -> (rec l. Unit + Text * l) |]
  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
Match -> [tyQ| a * b -> (a -> b -> c) -> c |]
  Const
Force -> [tyQ| {a} -> a |]
  Const
Pure -> [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 -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
Neq -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
Lt -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
Gt -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
Leq -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
Geq -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
cmpBinT
  Const
And -> [tyQ| Bool -> Bool -> Bool|]
  Const
Or -> [tyQ| Bool -> Bool -> Bool|]
  Const
Add -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
arithBinT
  Const
Sub -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
arithBinT
  Const
Mul -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
arithBinT
  Const
Div -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
arithBinT
  Const
Exp -> RawPolytype
forall {q :: ImplicitQuantification}. Poly q Type
arithBinT
  Const
Format -> [tyQ| a -> Text |]
  Const
Read -> [tyQ| Type -> Text -> a |]
  Const
Print -> [tyQ| Text -> Text -> Cmd Text |]
  Const
Erase -> [tyQ| Text -> Cmd 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
Warp -> [tyQ| Actor -> (Text * (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 :: Poly q Type
cmpBinT = [tyQ| a -> a -> Bool |]
  arithBinT :: Poly q Type
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 TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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) =>
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
  -- Once we're typechecking, we don't need to keep around explicit
  -- parens any more
  SParens Syntax
t1 -> Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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
  -- 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 TDCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 TDCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Type
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 TDCtx) sig m, Has (Reader [LocatedTCFrame]) sig m) =>
Syntax -> Sourced UType -> m (UType, UType)
decomposeFunTy Syntax
s (Source
Expected, UType
expected)
    Maybe Type
mxTy' <- (Type -> m Type) -> Maybe Type -> m (Maybe Type)
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) -> Maybe a -> f (Maybe b)
traverse (SrcLoc
-> (KindError -> TypeErr) -> ThrowC KindError m Type -> m Type
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 Type -> m Type)
-> (Type -> ThrowC KindError m Type) -> Type -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ThrowC KindError m Type
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) =>
Type -> m Type
processType) Maybe Type
mxTy
    Maybe UType -> (UType -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Maybe Type -> U (Maybe Type)
forall t. WithU t => t -> U t
toU Maybe Type
mxTy') ((UType -> m ()) -> m ()) -> (UType -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \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)
U.=:= 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 ()

    USyntax
body' <- forall v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding @Var @UPolytype (LocVar -> Var
forall v. Located v -> v
lvVar LocVar
x) (UType -> UPolytype
forall t (q :: ImplicitQuantification). t -> Poly q t
mkTrivPoly 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Type -> USyntax -> Term' UType
forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x Maybe Type
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 TDCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 RawPolytype
mxTy Maybe Polytype
_ 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
forall v. Located v -> v
lvVar LocVar
x)) (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall a b. (a -> b) -> a -> b
$ do
    Maybe Polytype
mqxTy <- (RawPolytype -> m Polytype)
-> Maybe RawPolytype -> m (Maybe Polytype)
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) -> Maybe a -> f (Maybe b)
traverse RawPolytype -> m Polytype
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) ty.
(Has (Reader TVCtx) sig m, Typical ty) =>
Poly 'Unquantified ty -> m (Poly 'Quantified ty)
quantify Maybe RawPolytype
mxTy
    ([Var]
skolems, UPolytype
upty, USyntax
t1') <- case Maybe Polytype
mqxTy 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' <- forall v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding @Var @UPolytype (LocVar -> Var
forall v. Located v -> v
lvVar LocVar
x) (UType -> UPolytype
forall t (q :: ImplicitQuantification). t -> Poly q t
mkTrivPoly 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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
        UType
uty' <- 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
t1) (UType -> UType -> TypeJoin
forall a. a -> a -> Join a
joined UType
xTy 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'
        ([Var], UPolytype, USyntax) -> m ([Var], 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. Perform
      -- implicit quantification, kind checking, and skolemization,
      -- then check definition and body under an extended context.
      Just Polytype
pty -> do
        TydefInfo Polytype
pty' Arity
_ <- 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 TDCtx) sig m, Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
processPolytype (Polytype -> m TydefInfo) -> Polytype -> m TydefInfo
forall a b. (a -> b) -> a -> b
$ Polytype
pty
        let upty :: U Polytype
upty = Polytype -> U Polytype
forall t. WithU t => t -> U t
toU Polytype
pty'
        (TVCtx
ss, UType
uty) <- UPolytype -> m (TVCtx, UType)
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader TVCtx) sig m) =>
UPolytype -> m (TVCtx, UType)
skolemize UPolytype
upty
        USyntax
t1' <- Var -> UPolytype -> m USyntax -> m USyntax
forall v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding (LocVar -> Var
forall v. Located v -> v
lvVar LocVar
x) UPolytype
upty (m USyntax -> m USyntax)
-> (m USyntax -> m USyntax) -> m USyntax -> m USyntax
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVCtx -> m USyntax -> m USyntax
forall v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
Ctx v t -> m a -> m a
withBindings TVCtx
ss (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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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
        ([Var], UPolytype, USyntax) -> m ([Var], UPolytype, USyntax)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVCtx -> [Var]
forall v t. Ctx v t -> [v]
Ctx.vars TVCtx
ss, UPolytype
upty, USyntax
t1')

    -- Check the requirements of t1.
    TDCtx
tdCtx <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @TDCtx
    Ctx Var 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 = TDCtx -> Ctx Var Requirements -> Term -> Requirements
requirements TDCtx
tdCtx Ctx Var 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 pure, like
    -- 'pure (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 TDCtx) 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 v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding (LocVar -> Var
forall v. Located v -> v
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 v t (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
(Has (Reader (Ctx v t)) sig m, Ord v, Hashable v, Hashable t) =>
v -> t -> m a -> m a
withBinding (LocVar -> Var
forall v. Located v -> v
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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 none of the generated 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 -> [Var] -> UPolytype -> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has Unification sig m, Has (Reader [LocatedTCFrame]) sig m,
 Has (Throw ContextualTypeErr) sig m) =>
SrcLoc -> [Var] -> UPolytype -> m ()
noSkolems SrcLoc
l [Var]
skolems)

    -- 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; pure (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; pure (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 RawPolytype
-> Maybe Polytype
-> Maybe Requirements
-> USyntax
-> USyntax
-> Term' UType
forall ty.
LetSyntax
-> Bool
-> LocVar
-> Maybe RawPolytype
-> Maybe Polytype
-> Maybe Requirements
-> Syntax' ty
-> Syntax' ty
-> Term' ty
SLet LetSyntax
ls Bool
r LocVar
x Maybe RawPolytype
mxTy Maybe Polytype
mqxTy 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 Located TDVar
x Polytype
pty Maybe TydefInfo
_ Syntax
t1 -> do
    tydef :: TydefInfo
tydef@(TydefInfo Polytype
pty' Arity
_) <- 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 TDCtx) sig m, Has (Throw KindError) sig m) =>
Polytype -> m TydefInfo
processPolytype Polytype
pty
    USyntax
t1' <- Var -> TydefInfo -> m USyntax -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Reader TDCtx) sig m =>
Var -> TydefInfo -> m a -> m a
withBindingTD (TDVar -> Var
tdVarName (Located TDVar -> TDVar
forall v. Located v -> v
lvVar Located TDVar
x)) TydefInfo
tydef (Syntax -> UType -> m USyntax
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader UCtx) sig m,
 Has (Reader (Ctx Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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' <- TDVar -> TydefInfo -> UType -> UType
forall t. Typical t => TDVar -> TydefInfo -> t -> t
elimTydef (Located TDVar -> TDVar
forall v. Located v -> v
lvVar Located TDVar
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 (Located TDVar
-> Polytype -> Maybe TydefInfo -> USyntax -> Term' UType
forall ty.
Located TDVar
-> Polytype -> Maybe TydefInfo -> Syntax' ty -> Term' ty
STydef Located TDVar
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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 TDCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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 Var Requirements)) sig m,
 Has (Reader TDCtx) sig m, Has (Reader TVCtx) 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
  TAntiSyn {} -> 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
  TRequire {} -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
  TStock {} -> 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
  TType {} -> 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, delay, and parens 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
  SParens 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
forall v. Located v -> v
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 v t. Ord v => v -> Ctx v 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 RawPolytype
_ -> 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 (UPolytype -> ([Var], UType)
forall t. Poly 'Quantified t -> ([Var], t)
unPoly -> ([], 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
  Free.Pure {} -> Bool
False
  Free.Free {} -> Bool
False