{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Swarm.Language.Typecheck (
ContextualTypeErr (..),
TypeErr (..),
InvalidAtomicReason (..),
Source (..),
withSource,
Join,
getJoin,
TCFrame (..),
LocatedTCFrame (..),
TCStack,
withFrame,
getTCStack,
TC,
runTC,
fresh,
substU,
unify,
HasBindings (..),
instantiate,
skolemize,
generalize,
inferTop,
inferModule,
infer,
inferConst,
check,
isSimpleUType,
) where
import Control.Arrow ((***))
import Control.Category ((>>>))
import Control.Lens ((^.))
import Control.Lens.Indexed (itraverse)
import Control.Monad (forM_, void, when, (<=<))
import Control.Monad.Except (
ExceptT,
MonadError (catchError, throwError),
runExceptT,
)
import Control.Monad.Reader (
MonadReader (ask, local),
ReaderT (runReaderT),
mapReaderT,
)
import Control.Monad.Trans.Class (MonadTrans (lift))
import Control.Unification hiding (applyBindings, unify, (=:=))
import Control.Unification qualified as U
import Control.Unification.IntVar
import Data.Data (Data, gmapM)
import Data.Foldable (fold)
import Data.Functor.Identity
import Data.Generics (mkM)
import Data.Map (Map, (!))
import Data.Map qualified as M
import Data.Maybe
import Data.Set (Set, (\\))
import Data.Set qualified as S
import Data.Text qualified as T
import Swarm.Language.Context hiding (lookup)
import Swarm.Language.Context qualified as Ctx
import Swarm.Language.Module
import Swarm.Language.Parse.QQ (tyQ)
import Swarm.Language.Syntax
import Swarm.Language.Typecheck.Unify
import Swarm.Language.Types
import Prelude hiding (lookup)
data TCFrame where
TCDef :: Var -> TCFrame
TCBindL :: TCFrame
TCBindR :: TCFrame
deriving (Int -> TCFrame -> ShowS
[TCFrame] -> ShowS
TCFrame -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCFrame] -> ShowS
$cshowList :: [TCFrame] -> ShowS
show :: TCFrame -> String
$cshow :: TCFrame -> String
showsPrec :: Int -> TCFrame -> ShowS
$cshowsPrec :: Int -> TCFrame -> ShowS
Show)
data LocatedTCFrame = LocatedTCFrame SrcLoc TCFrame
deriving (Int -> LocatedTCFrame -> ShowS
TCStack -> ShowS
LocatedTCFrame -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: TCStack -> ShowS
$cshowList :: TCStack -> ShowS
show :: LocatedTCFrame -> String
$cshow :: LocatedTCFrame -> String
showsPrec :: Int -> LocatedTCFrame -> ShowS
$cshowsPrec :: Int -> LocatedTCFrame -> ShowS
Show)
type TCStack = [LocatedTCFrame]
data Source
=
Expected
|
Actual
deriving (Int -> Source -> ShowS
[Source] -> ShowS
Source -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Source] -> ShowS
$cshowList :: [Source] -> ShowS
show :: Source -> String
$cshow :: Source -> String
showsPrec :: Int -> Source -> ShowS
$cshowsPrec :: Int -> Source -> ShowS
Show, Source -> Source -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Source -> Source -> Bool
$c/= :: Source -> Source -> Bool
== :: Source -> Source -> Bool
$c== :: Source -> Source -> Bool
Eq, Eq Source
Source -> Source -> Bool
Source -> Source -> Ordering
Source -> Source -> Source
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Source -> Source -> Source
$cmin :: Source -> Source -> Source
max :: Source -> Source -> Source
$cmax :: Source -> Source -> Source
>= :: Source -> Source -> Bool
$c>= :: Source -> Source -> Bool
> :: Source -> Source -> Bool
$c> :: Source -> Source -> Bool
<= :: Source -> Source -> Bool
$c<= :: Source -> Source -> Bool
< :: Source -> Source -> Bool
$c< :: Source -> Source -> Bool
compare :: Source -> Source -> Ordering
$ccompare :: Source -> Source -> Ordering
Ord, Source
forall a. a -> a -> Bounded a
maxBound :: Source
$cmaxBound :: Source
minBound :: Source
$cminBound :: Source
Bounded, Int -> Source
Source -> Int
Source -> [Source]
Source -> Source
Source -> Source -> [Source]
Source -> Source -> Source -> [Source]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Source -> Source -> Source -> [Source]
$cenumFromThenTo :: Source -> Source -> Source -> [Source]
enumFromTo :: Source -> Source -> [Source]
$cenumFromTo :: Source -> Source -> [Source]
enumFromThen :: Source -> Source -> [Source]
$cenumFromThen :: Source -> Source -> [Source]
enumFrom :: Source -> [Source]
$cenumFrom :: Source -> [Source]
fromEnum :: Source -> Int
$cfromEnum :: Source -> Int
toEnum :: Int -> Source
$ctoEnum :: Int -> Source
pred :: Source -> Source
$cpred :: Source -> Source
succ :: Source -> Source
$csucc :: Source -> Source
Enum)
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
type Sourced a = (Source, a)
newtype Join a = Join (Source -> a)
instance (Show a) => Show (Join a) where
show :: Join a -> String
show (forall a. Join a -> (a, a)
getJoin -> (a
e, a
a)) = String
"(expected: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
e forall a. Semigroup a => a -> a -> a
<> String
", actual: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
a forall a. Semigroup a => a -> a -> a
<> String
")"
type TypeJoin = Join UType
joined :: a -> a -> Join a
joined :: forall a. a -> a -> Join a
joined a
expect a
actual = forall a. (Source -> a) -> Join a
Join (\case Source
Expected -> a
expect; Source
Actual -> a
actual)
mkJoin :: Sourced a -> a -> Join a
mkJoin :: forall a. Sourced a -> a -> Join a
mkJoin (Source
src, a
a1) a
a2 = forall a. (Source -> a) -> Join a
Join forall a b. (a -> b) -> a -> b
$ \Source
s -> if Source
s forall a. Eq a => a -> a -> Bool
== Source
src then a
a1 else a
a2
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 TC = ReaderT UCtx (ReaderT TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
withFrame :: SrcLoc -> TCFrame -> TC a -> TC a
withFrame :: forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
f = forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT (forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (SrcLoc -> TCFrame -> LocatedTCFrame
LocatedTCFrame SrcLoc
l TCFrame
f forall a. a -> [a] -> [a]
:))
getTCStack :: TC TCStack
getTCStack :: TC TCStack
getTCStack = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask
runTC :: TCtx -> TC UModule -> Either ContextualTypeErr TModule
runTC :: Ctx Polytype -> TC UModule -> Either ContextualTypeErr TModule
runTC Ctx Polytype
ctx =
(forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall u. HasBindings u => u -> TC u
applyBindings)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ( forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\(Module Syntax' (UTerm TypeF IntVar)
u UCtx
uctx) ->
forall s t. Syntax' s -> Ctx t -> Module s t
Module
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. Maybe a -> TC a
checkPredicative forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. WithU t => U t -> Maybe t
fromU forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTerm TypeF IntVar -> TC UPolytype
generalize)) Syntax' (UTerm TypeF IntVar)
u
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Maybe a -> TC a
checkPredicative (forall t. WithU t => U t -> Maybe t
fromU UCtx
uctx)
)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall t. WithU t => t -> U t
toU Ctx Polytype
ctx)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT []
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall a. Identity a -> a
runIdentity
checkPredicative :: Maybe a -> TC a
checkPredicative :: forall a. Maybe a -> TC a
checkPredicative = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeErr -> ContextualTypeErr
mkRawTypeErr TypeErr
Impredicative)) forall (f :: * -> *) a. Applicative f => a -> f a
pure
lookup :: SrcLoc -> Var -> TC UType
lookup :: SrcLoc -> Var -> TC (UTerm TypeF IntVar)
lookup SrcLoc
loc Var
x = do
UCtx
ctx <- TC UCtx
getCtx
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
loc forall a b. (a -> b) -> a -> b
$ Var -> TypeErr
UnboundVar Var
x) UPolytype -> TC (UTerm TypeF IntVar)
instantiate (forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x UCtx
ctx)
getCtx :: TC UCtx
getCtx :: TC UCtx
getCtx = forall r (m :: * -> *). MonadReader r m => m r
ask
addLocToTypeErr :: SrcLoc -> TC a -> TC a
addLocToTypeErr :: forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l TC a
m =
TC a
m forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
CTE SrcLoc
NoLoc TCStack
_ TypeErr
te -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l TypeErr
te
ContextualTypeErr
te -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ContextualTypeErr
te
deriving instance Ord IntVar
class FreeVars a where
freeVars :: a -> TC (Set IntVar)
instance FreeVars UType where
freeVars :: UTerm TypeF IntVar -> TC (Set IntVar)
freeVars UTerm TypeF IntVar
ut = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UTerm TypeF IntVar
ut
instance (FreeVars t) => FreeVars (Poly t) where
freeVars :: Poly t -> TC (Set IntVar)
freeVars (Forall [Var]
_ t
t) = forall a. FreeVars a => a -> TC (Set IntVar)
freeVars t
t
instance FreeVars UCtx where
freeVars :: UCtx -> TC (Set IntVar)
freeVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. FreeVars a => a -> TC (Set IntVar)
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Ctx t -> Map Var t
unCtx
fresh :: TC UType
fresh :: TC (UTerm TypeF IntVar)
fresh = forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar)
substU :: Map (Either Var IntVar) UType -> UType -> UType
substU :: Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU Map (Either Var IntVar) (UTerm TypeF IntVar)
m =
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
(\IntVar
v -> forall a. a -> Maybe a -> a
fromMaybe (forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. b -> Either a b
Right IntVar
v) Map (Either Var IntVar) (UTerm TypeF IntVar)
m))
( \case
TyVarF Var
v -> forall a. a -> Maybe a -> a
fromMaybe (Var -> UTerm TypeF IntVar
UTyVar Var
v) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall a b. a -> Either a b
Left Var
v) Map (Either Var IntVar) (UTerm TypeF IntVar)
m)
TypeF (UTerm TypeF IntVar)
f -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeF (UTerm TypeF IntVar)
f
)
noSkolems :: SrcLoc -> UPolytype -> TC ()
noSkolems :: SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l (Forall [Var]
xs UTerm TypeF IntVar
upty) = do
UTerm TypeF IntVar
upty' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
upty
let tyvs :: Set Var
tyvs =
forall (t :: * -> *) v a.
Functor t =>
(v -> a) -> (t a -> a) -> UTerm t v -> a
ucata
(forall a b. a -> b -> a
const forall a. Set a
S.empty)
(\case TyVarF Var
v -> forall a. a -> Set a
S.singleton Var
v; TypeF (Set Var)
f -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TypeF (Set Var)
f)
UTerm TypeF IntVar
upty'
ftyvs :: Set Var
ftyvs = Set Var
tyvs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> Maybe a
S.lookupMin Set Var
ftyvs) forall a b. (a -> b) -> a -> b
$ forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> TypeErr
EscapedSkolem
infix 4 =:=
unify :: Maybe Syntax -> TypeJoin -> TC UType
unify :: Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify Maybe Syntax
ms TypeJoin
j = case UTerm TypeF IntVar -> UTerm TypeF IntVar -> UnifyStatus
unifyCheck UTerm TypeF IntVar
expected UTerm TypeF IntVar
actual of
UnifyStatus
Apart -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
NoLoc forall a b. (a -> b) -> a -> b
$ Maybe Syntax -> TypeJoin -> TypeErr
Mismatch Maybe Syntax
ms TypeJoin
j
UnifyStatus
Equal -> forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
expected
UnifyStatus
MightUnify -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
expected forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
U.=:= UTerm TypeF IntVar
actual
where
(UTerm TypeF IntVar
expected, UTerm TypeF IntVar
actual) = forall a. Join a -> (a, a)
getJoin TypeJoin
j
(=:=) :: UType -> UType -> TC UType
UTerm TypeF IntVar
ty1 =:= :: UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
ty2 = Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify forall a. Maybe a
Nothing (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2)
class HasBindings u where
applyBindings :: u -> TC u
instance HasBindings UType where
applyBindings :: UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
applyBindings = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
U.applyBindings
instance HasBindings UPolytype where
applyBindings :: UPolytype -> TC UPolytype
applyBindings (Forall [Var]
xs UTerm TypeF IntVar
u) = forall t. [Var] -> t -> Poly t
Forall [Var]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
u
instance HasBindings UCtx where
applyBindings :: UCtx -> TC UCtx
applyBindings = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall u. HasBindings u => u -> TC u
applyBindings
instance (HasBindings u, Data u) => HasBindings (Term' u) where
applyBindings :: Term' u -> TC (Term' u)
applyBindings = forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> a -> m a
gmapM (forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM (forall u. HasBindings u => u -> TC u
applyBindings @(Syntax' u)))
instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
applyBindings :: Syntax' u -> TC (Syntax' u)
applyBindings (Syntax' SrcLoc
l Term' u
t u
u) = forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings Term' u
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> TC u
applyBindings u
u
instance HasBindings UModule where
applyBindings :: UModule -> TC UModule
applyBindings (Module Syntax' (UTerm TypeF IntVar)
u UCtx
uctx) = forall s t. Syntax' s -> Ctx t -> Module s t
Module forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall u. HasBindings u => u -> TC u
applyBindings Syntax' (UTerm TypeF IntVar)
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall u. HasBindings u => u -> TC u
applyBindings UCtx
uctx
instantiate :: UPolytype -> TC UType
instantiate :: UPolytype -> TC (UTerm TypeF IntVar)
instantiate (Forall [Var]
xs UTerm TypeF IntVar
uty) = do
[UTerm TypeF IntVar]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const TC (UTerm TypeF IntVar)
fresh) [Var]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) [UTerm TypeF IntVar]
xs')) UTerm TypeF IntVar
uty
skolemize :: UPolytype -> TC UType
skolemize :: UPolytype -> TC (UTerm TypeF IntVar)
skolemize (Forall [Var]
xs UTerm TypeF IntVar
uty) = do
[UTerm TypeF IntVar]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const TC (UTerm TypeF IntVar)
fresh) [Var]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left [Var]
xs) (forall a b. (a -> b) -> [a] -> [b]
map forall {t :: * -> *}.
Show (t (UTerm t IntVar)) =>
UTerm t IntVar -> UTerm TypeF IntVar
toSkolem [UTerm TypeF IntVar]
xs'))) UTerm TypeF IntVar
uty
where
toSkolem :: UTerm t IntVar -> UTerm TypeF IntVar
toSkolem (UVar IntVar
v) = Var -> UTerm TypeF IntVar
UTyVar (Var -> IntVar -> Var
mkVarName Var
"s" IntVar
v)
toSkolem UTerm t IntVar
x = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Non-UVar in skolemize.toSkolem: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UTerm t IntVar
x
generalize :: UType -> TC UPolytype
generalize :: UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
uty = do
UTerm TypeF IntVar
uty' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
uty
UCtx
ctx <- TC UCtx
getCtx
Set IntVar
tmfvs <- forall a. FreeVars a => a -> TC (Set IntVar)
freeVars UTerm TypeF IntVar
uty'
Set IntVar
ctxfvs <- forall a. FreeVars a => a -> TC (Set IntVar)
freeVars UCtx
ctx
let fvs :: [IntVar]
fvs = forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ Set IntVar
tmfvs forall a. Ord a => Set a -> Set a -> Set a
\\ Set IntVar
ctxfvs
alphabet :: String
alphabet = [Char
'a' .. Char
'z']
prettyNames :: [Var]
prettyNames = forall a b. (a -> b) -> [a] -> [b]
map String -> Var
T.pack (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
: []) String
alphabet forall a. [a] -> [a] -> [a]
++ [Char
x forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
n | Int
n <- [Int
0 :: Int ..], Char
x <- String
alphabet])
renaming :: [(IntVar, Var)]
renaming = forall a b. [a] -> [b] -> [(a, b)]
zip [IntVar]
fvs [Var]
prettyNames
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
forall t. [Var] -> t -> Poly t
Forall
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(IntVar, Var)]
renaming)
(Map (Either Var IntVar) (UTerm TypeF IntVar)
-> UTerm TypeF IntVar -> UTerm TypeF IntVar
substU (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. b -> Either a b
Right forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Var -> UTerm TypeF IntVar
UTyVar) forall a b. (a -> b) -> a -> b
$ [(IntVar, Var)]
renaming) UTerm TypeF IntVar
uty')
data ContextualTypeErr = CTE {ContextualTypeErr -> SrcLoc
cteSrcLoc :: SrcLoc, ContextualTypeErr -> TCStack
cteStack :: TCStack, ContextualTypeErr -> TypeErr
cteTypeErr :: TypeErr}
deriving (Int -> ContextualTypeErr -> ShowS
[ContextualTypeErr] -> ShowS
ContextualTypeErr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ContextualTypeErr] -> ShowS
$cshowList :: [ContextualTypeErr] -> ShowS
show :: ContextualTypeErr -> String
$cshow :: ContextualTypeErr -> String
showsPrec :: Int -> ContextualTypeErr -> ShowS
$cshowsPrec :: Int -> ContextualTypeErr -> ShowS
Show)
mkRawTypeErr :: TypeErr -> ContextualTypeErr
mkRawTypeErr :: TypeErr -> ContextualTypeErr
mkRawTypeErr = SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
CTE SrcLoc
NoLoc []
mkTypeErr :: SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr :: SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr = SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
CTE
throwTypeErr :: SrcLoc -> TypeErr -> TC a
throwTypeErr :: forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l TypeErr
te = do
TCStack
stk <- TC TCStack
getTCStack
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SrcLoc -> TCStack -> TypeErr -> ContextualTypeErr
mkTypeErr SrcLoc
l TCStack
stk TypeErr
te
data TypeErr
=
UnboundVar Var
|
EscapedSkolem Var
|
Infinite IntVar UType
|
UnifyErr (TypeF UType) (TypeF UType)
|
Mismatch (Maybe Syntax) TypeJoin
|
LambdaArgMismatch TypeJoin
|
FieldsMismatch (Join (Set Var))
|
DefNotTopLevel Term
|
CantInfer Term
|
CantInferProj Term
|
UnknownProj Var Term
|
InvalidAtomic InvalidAtomicReason Term
|
Impredicative
deriving (Int -> TypeErr -> ShowS
[TypeErr] -> ShowS
TypeErr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeErr] -> ShowS
$cshowList :: [TypeErr] -> ShowS
show :: TypeErr -> String
$cshow :: TypeErr -> String
showsPrec :: Int -> TypeErr -> ShowS
$cshowsPrec :: Int -> TypeErr -> ShowS
Show)
data InvalidAtomicReason
=
TooManyTicks Int
|
AtomicDupingThing
|
NonSimpleVarType Var UPolytype
|
NestedAtomic
|
LongConst
deriving (Int -> InvalidAtomicReason -> ShowS
[InvalidAtomicReason] -> ShowS
InvalidAtomicReason -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InvalidAtomicReason] -> ShowS
$cshowList :: [InvalidAtomicReason] -> ShowS
show :: InvalidAtomicReason -> String
$cshow :: InvalidAtomicReason -> String
showsPrec :: Int -> InvalidAtomicReason -> ShowS
$cshowsPrec :: Int -> InvalidAtomicReason -> ShowS
Show)
instance Fallible TypeF IntVar ContextualTypeErr where
occursFailure :: IntVar -> UTerm TypeF IntVar -> ContextualTypeErr
occursFailure IntVar
v UTerm TypeF IntVar
t = TypeErr -> ContextualTypeErr
mkRawTypeErr (IntVar -> UTerm TypeF IntVar -> TypeErr
Infinite IntVar
v UTerm TypeF IntVar
t)
mismatchFailure :: TypeF (UTerm TypeF IntVar)
-> TypeF (UTerm TypeF IntVar) -> ContextualTypeErr
mismatchFailure TypeF (UTerm TypeF IntVar)
t1 TypeF (UTerm TypeF IntVar)
t2 = TypeErr -> ContextualTypeErr
mkRawTypeErr (TypeF (UTerm TypeF IntVar) -> TypeF (UTerm TypeF IntVar) -> TypeErr
UnifyErr TypeF (UTerm TypeF IntVar)
t1 TypeF (UTerm TypeF IntVar)
t2)
decomposeDelayTy :: Syntax -> Sourced UType -> TC UType
decomposeDelayTy :: Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeDelayTy Syntax
_ (Source
_, UTyDelay UTerm TypeF IntVar
a) = forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeDelayTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
UTerm TypeF IntVar
a <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyDelay UTerm TypeF IntVar
a))
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeCmdTy :: Syntax -> Sourced UType -> TC UType
decomposeCmdTy :: Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
_ (Source
_, UTyCmd UTerm TypeF IntVar
a) = forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeCmdTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
UTerm TypeF IntVar
a <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
a))
forall (m :: * -> *) a. Monad m => a -> m a
return UTerm TypeF IntVar
a
decomposeFunTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeFunTy :: Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
_ (Source
_, UTyFun UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2) = forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
decomposeFunTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
UTerm TypeF IntVar
ty1 <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
ty2 <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2))
forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
decomposeProdTy :: Syntax -> Sourced UType -> TC (UType, UType)
decomposeProdTy :: Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeProdTy Syntax
_ (Source
_, UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2) = forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
decomposeProdTy Syntax
t Sourced (UTerm TypeF IntVar)
ty = do
UTerm TypeF IntVar
ty1 <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
ty2 <- TC (UTerm TypeF IntVar)
fresh
UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t) (forall a. Sourced a -> a -> Join a
mkJoin Sourced (UTerm TypeF IntVar)
ty (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2))
forall (m :: * -> *) a. Monad m => a -> m a
return (UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2)
inferTop :: TCtx -> Syntax -> Either ContextualTypeErr TModule
inferTop :: Ctx Polytype -> Syntax -> Either ContextualTypeErr TModule
inferTop Ctx Polytype
ctx = Ctx Polytype -> TC UModule -> Either ContextualTypeErr TModule
runTC Ctx Polytype
ctx forall b c a. (b -> c) -> (a -> b) -> a -> c
. Syntax -> TC UModule
inferModule
inferModule :: Syntax -> TC UModule
inferModule :: Syntax -> TC UModule
inferModule s :: Syntax
s@(Syntax SrcLoc
l Term
t) = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
SDef Bool
r LocVar
x Maybe Polytype
Nothing Syntax
t1 -> forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l (Var -> TCFrame
TCDef (LocVar -> Var
lvVar LocVar
x)) forall a b. (a -> b) -> a -> b
$ do
UTerm TypeF IntVar
xTy <- TC (UTerm TypeF IntVar)
fresh
Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
UTerm TypeF IntVar
_ <- Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
t1) (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
xTy (Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
UPolytype
pty <- UTerm TypeF IntVar -> TC UPolytype
generalize (Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x forall a. Maybe a
Nothing Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
pty)
SDef Bool
r LocVar
x (Just Polytype
pty) Syntax
t1 -> forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l (Var -> TCFrame
TCDef (LocVar -> Var
lvVar LocVar
x)) forall a b. (a -> b) -> a -> b
$ do
let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
t1 UTerm TypeF IntVar
uty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s t. Syntax' s -> Ctx t -> Module s t
Module (forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool -> LocVar -> Maybe Polytype -> Syntax' ty -> Term' ty
SDef Bool
r LocVar
x (forall a. a -> Maybe a
Just Polytype
pty) Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)) (forall t. Var -> t -> Ctx t
singleton (LocVar -> Var
lvVar LocVar
x) UPolytype
upty)
SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
Module Syntax' (UTerm TypeF IntVar)
c1' UCtx
ctx1 <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindL forall a b. (a -> b) -> a -> b
$ Syntax -> TC UModule
inferModule Syntax
c1
UTerm TypeF IntVar
a <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c1 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
UPolytype
genA <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
a
forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Ctx t -> m a -> m a
withBindings UCtx
ctx1 forall a b. (a -> b) -> a -> b
$
forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx forall a b. (a -> b) -> a -> b
$ do
Module Syntax' (UTerm TypeF IntVar)
c2' UCtx
ctx2 <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindR forall a b. (a -> b) -> a -> b
$ Syntax -> TC UModule
inferModule Syntax
c2
UTerm TypeF IntVar
_ <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c2 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
let ctxX :: UCtx
ctxX = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall t. Ctx t
Ctx.empty ((forall t. Var -> t -> Ctx t
`Ctx.singleton` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
forall s t. Syntax' s -> Ctx t -> Module s t
Module
(forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' (UTerm TypeF IntVar)
c1' Syntax' (UTerm TypeF IntVar)
c2') (Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
(UCtx
ctx1 forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctxX forall t. Ctx t -> Ctx t -> Ctx t
`Ctx.union` UCtx
ctx2)
Term
_anyOtherTerm -> forall s t. Syntax' s -> Module s t
trivMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
s
infer :: Syntax -> TC (Syntax' UType)
infer :: Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer s :: Syntax
s@(Syntax SrcLoc
l Term
t) = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
Term
TUnit -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l forall ty. Term' ty
TUnit UTerm TypeF IntVar
UTyUnit
TConst Const
c -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UPolytype -> TC (UTerm TypeF IntVar)
instantiate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. WithU t => t -> U t
toU forall a b. (a -> b) -> a -> b
$ Const -> Polytype
inferConst Const
c)
TDir Direction
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Direction -> Term' ty
TDir Direction
d) UTerm TypeF IntVar
UTyDir
TInt Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Integer -> Term' ty
TInt Integer
n) UTerm TypeF IntVar
UTyInt
TAntiInt Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiInt Var
x) UTerm TypeF IntVar
UTyInt
TText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TText Var
x) UTerm TypeF IntVar
UTyText
TAntiText Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TAntiText Var
x) UTerm TypeF IntVar
UTyText
TBool Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Bool -> Term' ty
TBool Bool
b) UTerm TypeF IntVar
UTyBool
TRobot Int
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Term' ty
TRobot Int
r) UTerm TypeF IntVar
UTyActor
TRequireDevice Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TRequireDevice Var
d) (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)
TRequire Int
n Var
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Int -> Var -> Term' ty
TRequire Int
n Var
d) (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)
SRequirements Var
x Syntax
t1 -> do
Syntax' (UTerm TypeF IntVar)
t1' <- Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Syntax' ty -> Term' ty
SRequirements Var
x Syntax' (UTerm TypeF IntVar)
t1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
UTyUnit)
TRef Int
_ -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInfer Term
t
TVar Var
x -> forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Var -> Term' ty
TVar Var
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcLoc -> Var -> TC (UTerm TypeF IntVar)
lookup SrcLoc
l Var
x
SLam LocVar
x (Just Type
argTy) Syntax
body -> do
let uargTy :: U Type
uargTy = forall t. WithU t => t -> U t
toU Type
argTy
Syntax' (UTerm TypeF IntVar)
body' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
uargTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
body
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x (forall a. a -> Maybe a
Just Type
argTy) Syntax' (UTerm TypeF IntVar)
body') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
uargTy (Syntax' (UTerm TypeF IntVar)
body' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType))
TConst Const
c :$: Syntax
_
| Const
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> TC (UTerm TypeF IntVar)
fresh forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
s
SApp Syntax
f Syntax
x -> do
Syntax' (UTerm TypeF IntVar)
f' <- Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
f
(UTerm TypeF IntVar
argTy, UTerm TypeF IntVar
resTy) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
f (Source
Actual, Syntax' (UTerm TypeF IntVar)
f' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
Syntax' (UTerm TypeF IntVar)
x' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
x UTerm TypeF IntVar
argTy
UTerm TypeF IntVar
resTy' <- forall u. HasBindings u => u -> TC u
applyBindings UTerm TypeF IntVar
resTy
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' (UTerm TypeF IntVar)
f' Syntax' (UTerm TypeF IntVar)
x') UTerm TypeF IntVar
resTy'
SBind Maybe LocVar
mx Syntax
c1 Syntax
c2 -> do
Syntax' (UTerm TypeF IntVar)
c1' <- forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindL forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
c1
UTerm TypeF IntVar
a <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c1 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
UPolytype
genA <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
a
Syntax' (UTerm TypeF IntVar)
c2' <-
forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
`withBinding` UPolytype
genA) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SrcLoc -> TCFrame -> TC a -> TC a
withFrame SrcLoc
l TCFrame
TCBindR
forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
c2
UTerm TypeF IntVar
_ <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
c2 (Source
Actual, Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Maybe LocVar -> Syntax' ty -> Syntax' ty -> Term' ty
SBind Maybe LocVar
mx Syntax' (UTerm TypeF IntVar)
c1' Syntax' (UTerm TypeF IntVar)
c2') (Syntax' (UTerm TypeF IntVar)
c2' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
SProj Syntax
t1 Var
x -> do
Syntax' (UTerm TypeF IntVar)
t1' <- Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
case Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType of
UTyRcd Map Var (UTerm TypeF IntVar)
m -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var (UTerm TypeF IntVar)
m of
Just UTerm TypeF IntVar
xTy -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax' (UTerm TypeF IntVar)
t1' Var
x) UTerm TypeF IntVar
xTy
Maybe (UTerm TypeF IntVar)
Nothing -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Var -> Term -> TypeErr
UnknownProj Var
x (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax
t1 Var
x)
UTerm TypeF IntVar
_ -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInferProj (forall ty. Syntax' ty -> Var -> Term' ty
SProj Syntax
t1 Var
x)
SRcd Map Var (Maybe Syntax)
m -> do
Map Var (Syntax' (UTerm TypeF IntVar))
m' <- forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
itraverse (\Var
x -> Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x))) Map Var (Maybe Syntax)
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var (Syntax' (UTerm TypeF IntVar))
m')) (Map Var (UTerm TypeF IntVar) -> UTerm TypeF IntVar
UTyRcd (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType) Map Var (Syntax' (UTerm TypeF IntVar))
m'))
SAnnotate Syntax
c Polytype
pty -> do
let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
Syntax' (UTerm TypeF IntVar)
_ <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
c UTerm TypeF IntVar
uty
TC UCtx
getCtx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l)
UTerm TypeF IntVar
iuty <- UPolytype -> TC (UTerm TypeF IntVar)
instantiate UPolytype
upty
Syntax' (UTerm TypeF IntVar)
c' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
c UTerm TypeF IntVar
iuty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Polytype -> Term' ty
SAnnotate Syntax' (UTerm TypeF IntVar)
c' Polytype
pty) (Syntax' (UTerm TypeF IntVar)
c' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType)
Term
_ -> do
UTerm TypeF IntVar
sTy <- TC (UTerm TypeF IntVar)
fresh
Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
s UTerm TypeF IntVar
sTy
inferConst :: Const -> Polytype
inferConst :: Const -> Polytype
inferConst Const
c = case Const
c of
Const
Wait -> [tyQ| int -> cmd unit |]
Const
Noop -> [tyQ| cmd unit |]
Const
Selfdestruct -> [tyQ| cmd unit |]
Const
Move -> [tyQ| cmd unit |]
Const
Backup -> [tyQ| cmd unit |]
Const
Path -> [tyQ| (unit + int) -> ((int * int) + text) -> cmd (unit + dir) |]
Const
Push -> [tyQ| cmd unit |]
Const
Stride -> [tyQ| int -> cmd unit |]
Const
Turn -> [tyQ| dir -> cmd unit |]
Const
Grab -> [tyQ| cmd text |]
Const
Harvest -> [tyQ| cmd text |]
Const
Ignite -> [tyQ| dir -> cmd unit |]
Const
Place -> [tyQ| text -> cmd unit |]
Const
Ping -> [tyQ| actor -> cmd (unit + (int * int)) |]
Const
Give -> [tyQ| actor -> text -> cmd unit |]
Const
Equip -> [tyQ| text -> cmd unit |]
Const
Unequip -> [tyQ| text -> cmd unit |]
Const
Make -> [tyQ| text -> cmd unit |]
Const
Has -> [tyQ| text -> cmd bool |]
Const
Equipped -> [tyQ| text -> cmd bool |]
Const
Count -> [tyQ| text -> cmd int |]
Const
Reprogram -> [tyQ| actor -> {cmd a} -> cmd unit |]
Const
Build -> [tyQ| {cmd a} -> cmd actor |]
Const
Drill -> [tyQ| dir -> cmd (unit + text) |]
Const
Use -> [tyQ| text -> dir -> cmd (unit + text) |]
Const
Salvage -> [tyQ| cmd unit |]
Const
Say -> [tyQ| text -> cmd unit |]
Const
Listen -> [tyQ| cmd text |]
Const
Log -> [tyQ| text -> cmd unit |]
Const
View -> [tyQ| actor -> cmd unit |]
Const
Appear -> [tyQ| text -> cmd unit |]
Const
Create -> [tyQ| text -> cmd unit |]
Const
Halt -> [tyQ| actor -> cmd unit |]
Const
Time -> [tyQ| cmd int |]
Const
Scout -> [tyQ| dir -> cmd bool |]
Const
Whereami -> [tyQ| cmd (int * int) |]
Const
Waypoint -> [tyQ| text -> int -> cmd (int * (int * int)) |]
Const
Detect -> [tyQ| text -> ((int * int) * (int * int)) -> cmd (unit + (int * int)) |]
Const
Resonate -> [tyQ| text -> ((int * int) * (int * int)) -> cmd int |]
Const
Density -> [tyQ| ((int * int) * (int * int)) -> cmd int |]
Const
Sniff -> [tyQ| text -> cmd int |]
Const
Chirp -> [tyQ| text -> cmd dir |]
Const
Watch -> [tyQ| dir -> cmd unit |]
Const
Surveil -> [tyQ| (int * int) -> cmd unit |]
Const
Heading -> [tyQ| cmd dir |]
Const
Blocked -> [tyQ| cmd bool |]
Const
Scan -> [tyQ| dir -> cmd (unit + text) |]
Const
Upload -> [tyQ| actor -> cmd unit |]
Const
Ishere -> [tyQ| text -> cmd bool |]
Const
Isempty -> [tyQ| cmd bool |]
Const
Self -> [tyQ| actor |]
Const
Parent -> [tyQ| actor |]
Const
Base -> [tyQ| actor |]
Const
Meet -> [tyQ| cmd (unit + actor) |]
Const
MeetAll -> [tyQ| (b -> actor -> cmd b) -> b -> cmd b |]
Const
Whoami -> [tyQ| cmd text |]
Const
Setname -> [tyQ| text -> cmd unit |]
Const
Random -> [tyQ| int -> cmd int |]
Const
Run -> [tyQ| text -> cmd unit |]
Const
If -> [tyQ| bool -> {a} -> {a} -> a |]
Const
Inl -> [tyQ| a -> a + b |]
Const
Inr -> [tyQ| b -> a + b |]
Const
Case -> [tyQ|a + b -> (a -> c) -> (b -> c) -> c |]
Const
Fst -> [tyQ| a * b -> a |]
Const
Snd -> [tyQ| a * b -> b |]
Const
Force -> [tyQ| {a} -> a |]
Const
Return -> [tyQ| a -> cmd a |]
Const
Try -> [tyQ| {cmd a} -> {cmd a} -> cmd a |]
Const
Undefined -> [tyQ| a |]
Const
Fail -> [tyQ| text -> a |]
Const
Not -> [tyQ| bool -> bool |]
Const
Neg -> [tyQ| int -> int |]
Const
Eq -> Polytype
cmpBinT
Const
Neq -> Polytype
cmpBinT
Const
Lt -> Polytype
cmpBinT
Const
Gt -> Polytype
cmpBinT
Const
Leq -> Polytype
cmpBinT
Const
Geq -> Polytype
cmpBinT
Const
And -> [tyQ| bool -> bool -> bool|]
Const
Or -> [tyQ| bool -> bool -> bool|]
Const
Add -> Polytype
arithBinT
Const
Sub -> Polytype
arithBinT
Const
Mul -> Polytype
arithBinT
Const
Div -> Polytype
arithBinT
Const
Exp -> Polytype
arithBinT
Const
Format -> [tyQ| a -> text |]
Const
Concat -> [tyQ| text -> text -> text |]
Const
Chars -> [tyQ| text -> int |]
Const
Split -> [tyQ| int -> text -> (text * text) |]
Const
CharAt -> [tyQ| int -> text -> int |]
Const
ToChar -> [tyQ| int -> text |]
Const
AppF -> [tyQ| (a -> b) -> a -> b |]
Const
Swap -> [tyQ| text -> cmd text |]
Const
Atomic -> [tyQ| cmd a -> cmd a |]
Const
Instant -> [tyQ| cmd a -> cmd a |]
Const
Key -> [tyQ| text -> key |]
Const
InstallKeyHandler -> [tyQ| text -> (key -> cmd unit) -> cmd unit |]
Const
Teleport -> [tyQ| actor -> (int * int) -> cmd unit |]
Const
As -> [tyQ| actor -> {cmd a} -> cmd a |]
Const
RobotNamed -> [tyQ| text -> cmd actor |]
Const
RobotNumbered -> [tyQ| int -> cmd actor |]
Const
Knows -> [tyQ| text -> cmd bool |]
where
cmpBinT :: Polytype
cmpBinT = [tyQ| a -> a -> bool |]
arithBinT :: Polytype
arithBinT = [tyQ| int -> int -> int |]
check :: Syntax -> UType -> TC (Syntax' UType)
check :: Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check s :: Syntax
s@(Syntax SrcLoc
l Term
t) UTerm TypeF IntVar
expected = forall a. SrcLoc -> TC a -> TC a
addLocToTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ case Term
t of
SDelay DelayType
d Syntax
s1 -> do
UTerm TypeF IntVar
ty1 <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeDelayTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
Syntax' (UTerm TypeF IntVar)
s1' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
s1 UTerm TypeF IntVar
ty1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. DelayType -> Syntax' ty -> Term' ty
SDelay DelayType
d Syntax' (UTerm TypeF IntVar)
s1') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyDelay UTerm TypeF IntVar
ty1)
SPair Syntax
s1 Syntax
s2 -> do
(UTerm TypeF IntVar
ty1, UTerm TypeF IntVar
ty2) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeProdTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
Syntax' (UTerm TypeF IntVar)
s1' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
s1 UTerm TypeF IntVar
ty1
Syntax' (UTerm TypeF IntVar)
s2' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
s2 UTerm TypeF IntVar
ty2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SPair Syntax' (UTerm TypeF IntVar)
s1' Syntax' (UTerm TypeF IntVar)
s2') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2)
SLam LocVar
x Maybe Type
mxTy Syntax
body -> do
(UTerm TypeF IntVar
argTy, UTerm TypeF IntVar
resTy) <- Syntax
-> Sourced (UTerm TypeF IntVar)
-> TC (UTerm TypeF IntVar, UTerm TypeF IntVar)
decomposeFunTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
case forall t. WithU t => t -> U t
toU Maybe Type
mxTy of
Just UTerm TypeF IntVar
xTy -> case UTerm TypeF IntVar -> UTerm TypeF IntVar -> UnifyStatus
unifyCheck UTerm TypeF IntVar
argTy UTerm TypeF IntVar
xTy of
UnifyStatus
Apart -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ TypeJoin -> TypeErr
LambdaArgMismatch (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
argTy UTerm TypeF IntVar
xTy)
UnifyStatus
_ -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
argTy UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
xTy
Maybe (UTerm TypeF IntVar)
U (Maybe Type)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Syntax' (UTerm TypeF IntVar)
body' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
argTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
body UTerm TypeF IntVar
resTy
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. LocVar -> Maybe Type -> Syntax' ty -> Term' ty
SLam LocVar
x Maybe Type
mxTy Syntax' (UTerm TypeF IntVar)
body') (UTerm TypeF IntVar -> UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyFun UTerm TypeF IntVar
argTy UTerm TypeF IntVar
resTy)
TConst Const
c :$: Syntax
at
| Const
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Const
Atomic, Const
Instant] -> do
UTerm TypeF IntVar
argTy <- Syntax -> Sourced (UTerm TypeF IntVar) -> TC (UTerm TypeF IntVar)
decomposeCmdTy Syntax
s (Source
Expected, UTerm TypeF IntVar
expected)
Syntax' (UTerm TypeF IntVar)
at' <- Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
at (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
argTy)
Syntax' (UTerm TypeF IntVar)
atomic' <- Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer (SrcLoc -> Term -> Syntax
Syntax SrcLoc
l (forall ty. Const -> Term' ty
TConst Const
c))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Const
c forall a. Eq a => a -> a -> Bool
== Const
Atomic) forall a b. (a -> b) -> a -> b
$ Syntax -> TC ()
validAtomic Syntax
at
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Syntax' ty -> Syntax' ty -> Term' ty
SApp Syntax' (UTerm TypeF IntVar)
atomic' Syntax' (UTerm TypeF IntVar)
at') (UTerm TypeF IntVar -> UTerm TypeF IntVar
UTyCmd UTerm TypeF IntVar
argTy)
SLet Bool
r LocVar
x Maybe Polytype
mxTy Syntax
t1 Syntax
t2 -> do
(UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1') <- case Maybe Polytype
mxTy of
Maybe Polytype
Nothing -> do
UTerm TypeF IntVar
xTy <- TC (UTerm TypeF IntVar)
fresh
Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) (forall t. [Var] -> t -> Poly t
Forall [] UTerm TypeF IntVar
xTy) forall a b. (a -> b) -> a -> b
$ Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
t1
let uty :: UTerm TypeF IntVar
uty = Syntax' (UTerm TypeF IntVar)
t1' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType
UTerm TypeF IntVar
_ <- UTerm TypeF IntVar
xTy UTerm TypeF IntVar -> UTerm TypeF IntVar -> TC (UTerm TypeF IntVar)
=:= UTerm TypeF IntVar
uty
UPolytype
upty <- UTerm TypeF IntVar -> TC UPolytype
generalize UTerm TypeF IntVar
uty
forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1')
Just Polytype
pty -> do
let upty :: U Polytype
upty = forall t. WithU t => t -> U t
toU Polytype
pty
UTerm TypeF IntVar
uty <- UPolytype -> TC (UTerm TypeF IntVar)
skolemize UPolytype
upty
Syntax' (UTerm TypeF IntVar)
t1' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
t1 UTerm TypeF IntVar
uty
forall (m :: * -> *) a. Monad m => a -> m a
return (UPolytype
upty, Syntax' (UTerm TypeF IntVar)
t1')
Syntax' (UTerm TypeF IntVar)
t2' <- forall t (m :: * -> *) a.
MonadReader (Ctx t) m =>
Var -> t -> m a -> m a
withBinding (LocVar -> Var
lvVar LocVar
x) UPolytype
upty forall a b. (a -> b) -> a -> b
$ Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check Syntax
t2 UTerm TypeF IntVar
expected
TC UCtx
getCtx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SrcLoc -> UPolytype -> TC ()
noSkolems SrcLoc
l)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty.
Bool
-> LocVar -> Maybe Polytype -> Syntax' ty -> Syntax' ty -> Term' ty
SLet Bool
r LocVar
x Maybe Polytype
mxTy Syntax' (UTerm TypeF IntVar)
t1' Syntax' (UTerm TypeF IntVar)
t2') UTerm TypeF IntVar
expected
SDef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
DefNotTopLevel Term
t
SRcd Map Var (Maybe Syntax)
fields
| UTyRcd Map Var (UTerm TypeF IntVar)
tyMap <- UTerm TypeF IntVar
expected -> do
let expectedFields :: Set Var
expectedFields = forall k a. Map k a -> Set k
M.keysSet Map Var (UTerm TypeF IntVar)
tyMap
actualFields :: Set Var
actualFields = forall k a. Map k a -> Set k
M.keysSet Map Var (Maybe Syntax)
fields
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set Var
actualFields forall a. Eq a => a -> a -> Bool
/= Set Var
expectedFields) forall a b. (a -> b) -> a -> b
$
forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$
Join (Set Var) -> TypeErr
FieldsMismatch (forall a. a -> a -> Join a
joined Set Var
expectedFields Set Var
actualFields)
Map Var (Syntax' (UTerm TypeF IntVar))
m' <- forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
itraverse (\Var
x Maybe Syntax
ms -> Syntax
-> UTerm TypeF IntVar
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
check (forall a. a -> Maybe a -> a
fromMaybe (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x)) Maybe Syntax
ms) (Map Var (UTerm TypeF IntVar)
tyMap forall k a. Ord k => Map k a -> k -> a
! Var
x)) Map Var (Maybe Syntax)
fields
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l (forall ty. Map Var (Maybe (Syntax' ty)) -> Term' ty
SRcd (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var (Syntax' (UTerm TypeF IntVar))
m')) UTerm TypeF IntVar
expected
Term
_ -> do
Syntax' SrcLoc
l' Term' (UTerm TypeF IntVar)
t' UTerm TypeF IntVar
actual <- Syntax
-> ReaderT
UCtx
(ReaderT
TCStack (ExceptT ContextualTypeErr (IntBindingT TypeF Identity)))
(Syntax' (UTerm TypeF IntVar))
infer Syntax
s
forall ty. SrcLoc -> Term' ty -> ty -> Syntax' ty
Syntax' SrcLoc
l' Term' (UTerm TypeF IntVar)
t' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Syntax -> TypeJoin -> TC (UTerm TypeF IntVar)
unify (forall a. a -> Maybe a
Just Syntax
s) (forall a. a -> a -> Join a
joined UTerm TypeF IntVar
expected UTerm TypeF IntVar
actual)
validAtomic :: Syntax -> TC ()
validAtomic :: Syntax -> TC ()
validAtomic s :: Syntax
s@(Syntax SrcLoc
l Term
t) = do
Int
n <- Set Var -> Syntax -> TC Int
analyzeAtomic forall a. Set a
S.empty Syntax
s
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$ forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic (Int -> InvalidAtomicReason
TooManyTicks Int
n) Term
t
analyzeAtomic :: Set Var -> Syntax -> TC Int
analyzeAtomic :: Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals (Syntax SrcLoc
l Term
t) = case Term
t of
TUnit {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TDir {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TAntiInt {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TAntiText {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TBool {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRobot {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRequireDevice {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TRequire {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
SRequirements {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TConst Const
c
| Const
c forall a. Eq a => a -> a -> Bool
== Const
Atomic -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
NestedAtomic Term
t
| Const -> Bool
isLong Const
c -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
LongConst Term
t
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Const -> Bool
isTangible Const
c then Int
1 else Int
0
TConst Const
If :$: Syntax
tst :$: Syntax
thn :$: Syntax
els ->
forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
tst forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Ord a => a -> a -> a
max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
thn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
els)
SPair Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s2
SApp Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s2
SDelay DelayType
_ Syntax
s1 -> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1
SBind Maybe LocVar
mx Syntax
s1 Syntax
s2 -> forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Var -> Syntax -> TC Int
analyzeAtomic (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a. Ord a => a -> Set a -> Set a
S.insert forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocVar -> Var
lvVar) Maybe LocVar
mx Set Var
locals) Syntax
s2
SRcd Map Var (Maybe Syntax)
m -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, Maybe Syntax) -> TC Int
analyzeField (forall k a. Map k a -> [(k, a)]
M.assocs Map Var (Maybe Syntax)
m)
where
analyzeField :: (Var, Maybe Syntax) -> TC Int
analyzeField :: (Var, Maybe Syntax) -> TC Int
analyzeField (Var
x, Maybe Syntax
Nothing) = Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals (Term -> Syntax
STerm (forall ty. Var -> Term' ty
TVar Var
x))
analyzeField (Var
_, Just Syntax
s) = Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s
SProj {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
TVar Var
x
| Var
x forall a. Ord a => a -> Set a -> Bool
`S.member` Set Var
locals -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
| Bool
otherwise -> do
Maybe UPolytype
mxTy <- forall t. Var -> Ctx t -> Maybe t
Ctx.lookup Var
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TC UCtx
getCtx
case Maybe UPolytype
mxTy of
Maybe UPolytype
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
Just UPolytype
xTy -> do
UPolytype
xTy' <- forall u. HasBindings u => u -> TC u
applyBindings UPolytype
xTy
if UPolytype -> Bool
isSimpleUPolytype UPolytype
xTy'
then forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
else forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic (Var -> UPolytype -> InvalidAtomicReason
NonSimpleVarType Var
x UPolytype
xTy') Term
t
SLam {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
SLet {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
SDef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ InvalidAtomicReason -> Term -> TypeErr
InvalidAtomic InvalidAtomicReason
AtomicDupingThing Term
t
TRef {} -> forall a. SrcLoc -> TypeErr -> TC a
throwTypeErr SrcLoc
l forall a b. (a -> b) -> a -> b
$ Term -> TypeErr
CantInfer Term
t
SAnnotate Syntax
s Polytype
_ -> Set Var -> Syntax -> TC Int
analyzeAtomic Set Var
locals Syntax
s
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype :: UPolytype -> Bool
isSimpleUPolytype (Forall [] UTerm TypeF IntVar
ty) = UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty
isSimpleUPolytype UPolytype
_ = Bool
False
isSimpleUType :: UType -> Bool
isSimpleUType :: UTerm TypeF IntVar -> Bool
isSimpleUType = \case
UTyBase {} -> Bool
True
UTyVar {} -> Bool
False
UTySum UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2 -> UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty1 Bool -> Bool -> Bool
&& UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty2
UTyProd UTerm TypeF IntVar
ty1 UTerm TypeF IntVar
ty2 -> UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty1 Bool -> Bool -> Bool
&& UTerm TypeF IntVar -> Bool
isSimpleUType UTerm TypeF IntVar
ty2
UTyFun {} -> Bool
False
UTyCmd {} -> Bool
False
UTyDelay {} -> Bool
False
UVar {} -> Bool
False
UTerm {} -> Bool
False