{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE OverloadedStrings #-}

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

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

-- |
-- Module      :  Disco.Typecheck
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Typecheck the Disco surface language and transform it into a
-- type-annotated AST.
module Disco.Typecheck where

import Control.Arrow ((&&&))
import Control.Lens ((^..))
import Control.Monad.Except
import Control.Monad.Trans.Maybe
import Data.Bifunctor (first)
import Data.Coerce
import qualified Data.Foldable as F
import Data.List (group, sort)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (isJust)
import Data.Set (Set)
import qualified Data.Set as S
import Prelude as P hiding (lookup)

import Unbound.Generics.LocallyNameless (
  Alpha,
  Bind,
  Name,
  bind,
  embed,
  name2String,
  string2Name,
  substs,
  unembed,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

import Disco.Effects.Fresh
import Polysemy hiding (embed)
import Polysemy.Error
import Polysemy.Output
import Polysemy.Reader
import Polysemy.Writer

import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Context hiding (filter)
import qualified Disco.Context as Ctx
import Disco.Messages
import Disco.Module
import Disco.Names
import Disco.Subst (applySubst)
import qualified Disco.Subst as Subst
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Typecheck.Constraints
import Disco.Typecheck.Util
import Disco.Types
import Disco.Types.Rules

------------------------------------------------------------
-- Container utilities
------------------------------------------------------------

containerTy :: Container -> Type -> Type
containerTy :: Container -> Type -> Type
containerTy Container
c Type
ty = Con -> [Type] -> Type
TyCon (Container -> Con
containerToCon Container
c) [Type
ty]

containerToCon :: Container -> Con
containerToCon :: Container -> Con
containerToCon Container
ListContainer = Con
CList
containerToCon Container
BagContainer = Con
CBag
containerToCon Container
SetContainer = Con
CSet

------------------------------------------------------------
-- Telescopes
------------------------------------------------------------

-- | Infer the type of a telescope, given a way to infer the type of
--   each item along with a context of variables it binds; each such
--   context is then added to the overall context when inferring
--   subsequent items in the telescope.
inferTelescope ::
  (Alpha b, Alpha tyb, Member (Reader TyCtx) r) =>
  (b -> Sem r (tyb, TyCtx)) ->
  Telescope b ->
  Sem r (Telescope tyb, TyCtx)
inferTelescope :: forall b tyb (r :: EffectRow).
(Alpha b, Alpha tyb, Member (Reader TyCtx) r) =>
(b -> Sem r (tyb, TyCtx))
-> Telescope b -> Sem r (Telescope tyb, TyCtx)
inferTelescope b -> Sem r (tyb, TyCtx)
inferOne Telescope b
tel = do
  ([tyb]
tel1, TyCtx
ctx) <- [b] -> Sem r ([tyb], TyCtx)
go (forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope b
tel)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall b. Alpha b => [b] -> Telescope b
toTelescope [tyb]
tel1, TyCtx
ctx)
 where
  go :: [b] -> Sem r ([tyb], TyCtx)
go [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], forall a b. Ctx a b
emptyCtx)
  go (b
b : [b]
bs) = do
    (tyb
tyb, TyCtx
ctx) <- b -> Sem r (tyb, TyCtx)
inferOne b
b
    forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx forall a b. (a -> b) -> a -> b
$ do
      ([tyb]
tybs, TyCtx
ctx') <- [b] -> Sem r ([tyb], TyCtx)
go [b]
bs
      forall (m :: * -> *) a. Monad m => a -> m a
return (tyb
tyb forall a. a -> [a] -> [a]
: [tyb]
tybs, TyCtx
ctx forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx')

------------------------------------------------------------
-- Modules
------------------------------------------------------------

-- | Check all the types and extract all relevant info (docs,
--   properties, types) from a module, returning a 'ModuleInfo' record
--   on success.  This function does not handle imports at all; any
--   imports should already be checked and passed in as the second
--   argument.
checkModule ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r =>
  ModuleName ->
  Map ModuleName ModuleInfo ->
  Module ->
  Sem r ModuleInfo
checkModule :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error LocTCError, Fresh]
  r =>
ModuleName
-> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo
checkModule ModuleName
name Map ModuleName ModuleInfo
imports (Module Set Ext
es [String]
_ [Decl]
m [(Name Term, Docs)]
docs [Term]
terms) = do
  let ([TypeDecl]
typeDecls, [TermDefn]
defns, [TypeDefn]
tydefs) = [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
m
      importTyCtx :: TyCtx
importTyCtx = forall a. Monoid a => [a] -> a
mconcat (Map ModuleName ModuleInfo
imports forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyCtx
miTys)
      -- XXX this isn't right, if multiple modules define the same type synonyms.
      -- Need to use a normal Ctx for tydefs too.
      importTyDefnCtx :: TyDefCtx
importTyDefnCtx = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions (Map ModuleName ModuleInfo
imports forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyDefCtx
miTydefs)
  TyDefCtx
tyDefnCtx <- forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
[TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx [TypeDefn]
tydefs
  forall (r :: EffectRow) a.
Member (Reader TyDefCtx) r =>
TyDefCtx -> Sem r a -> Sem r a
withTyDefns (TyDefCtx
tyDefnCtx forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TyDefCtx
importTyDefnCtx) forall a b. (a -> b) -> a -> b
$ do
    TyCtx
tyCtx <- forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx ModuleName
name [TypeDecl]
typeDecls
    forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
importTyCtx forall a b. (a -> b) -> a -> b
$ forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
tyCtx forall a b. (a -> b) -> a -> b
$ do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error LocTCError] r =>
ModuleName -> TypeDefn -> Sem r ()
checkTyDefn ModuleName
name) [TypeDefn]
tydefs
      [Defn]
adefns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh,
    Output (Message ann)]
  r =>
ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name) [TermDefn]
defns
      let defnCtx :: Ctx ATerm Defn
defnCtx = forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name (forall a b. (a -> b) -> [a] -> [b]
map (Defn -> Name ATerm
getDefnName forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. a -> a
id) [Defn]
adefns)
          docCtx :: Ctx Term Docs
docCtx = forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name [(Name Term, Docs)]
docs
          dups :: [Name ATerm]
dups = forall a. Ord a => [a] -> [a]
filterDups forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Defn -> Name ATerm
getDefnName forall a b. (a -> b) -> a -> b
$ [Defn]
adefns
      case [Name ATerm]
dups of
        (Name ATerm
x : [Name ATerm]
_) -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ TCError -> LocTCError
noLoc forall a b. (a -> b) -> a -> b
$ Name Term -> TCError
DuplicateDefns (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x)
        [] -> do
          Ctx ATerm [ATerm]
aprops <- forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc forall a b. (a -> b) -> a -> b
$ forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docCtx -- XXX location?
          [(ATerm, PolyType)]
aterms <- forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop [Term]
terms -- XXX location?
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModuleName
-> Map ModuleName ModuleInfo
-> [QName Term]
-> Ctx Term Docs
-> Ctx ATerm [ATerm]
-> TyCtx
-> TyDefCtx
-> Ctx ATerm Defn
-> [(ATerm, PolyType)]
-> Set Ext
-> ModuleInfo
ModuleInfo ModuleName
name Map ModuleName ModuleInfo
imports (forall a b. (a -> b) -> [a] -> [b]
map ((ModuleName
name forall a. ModuleName -> Name a -> QName a
.-) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeDecl -> Name Term
getDeclName) [TypeDecl]
typeDecls) Ctx Term Docs
docCtx Ctx ATerm [ATerm]
aprops TyCtx
tyCtx TyDefCtx
tyDefnCtx Ctx ATerm Defn
defnCtx [(ATerm, PolyType)]
aterms Set Ext
es
 where
  getDefnName :: Defn -> Name ATerm
  getDefnName :: Defn -> Name ATerm
getDefnName (Defn Name ATerm
n [Type]
_ Type
_ [Clause]
_) = Name ATerm
n

  getDeclName :: TypeDecl -> Name Term
  getDeclName :: TypeDecl -> Name Term
getDeclName (TypeDecl Name Term
n PolyType
_) = Name Term
n

--------------------------------------------------
-- Type definitions

-- | Turn a list of type definitions into a 'TyDefCtx', checking
--   for duplicate names among the definitions and also any type
--   definitions already in the context.
makeTyDefnCtx :: Members '[Reader TyDefCtx, Error TCError] r => [TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
[TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx [TypeDefn]
tydefs = do
  TyDefCtx
oldTyDefs <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  let oldNames :: [String]
oldNames = forall k a. Map k a -> [k]
M.keys TyDefCtx
oldTyDefs
      newNames :: [String]
newNames = forall a b. (a -> b) -> [a] -> [b]
map (\(TypeDefn String
x [String]
_ Type
_) -> String
x) [TypeDefn]
tydefs
      dups :: [String]
dups = forall a. Ord a => [a] -> [a]
filterDups forall a b. (a -> b) -> a -> b
$ [String]
newNames forall a. [a] -> [a] -> [a]
++ [String]
oldNames

  let convert :: TypeDefn -> (String, TyDefBody)
convert (TypeDefn String
x [String]
args Type
body) =
        (String
x, [String] -> ([Type] -> Type) -> TyDefBody
TyDefBody [String]
args (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b a. Subst b a => [(Name b, b)] -> a -> a
substs Type
body forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a. String -> Name a
string2Name [String]
args)))

  case [String]
dups of
    (String
x : [String]
_) -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> TCError
DuplicateTyDefns String
x)
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeDefn -> (String, TyDefBody)
convert [TypeDefn]
tydefs

-- | Check the validity of a type definition.
checkTyDefn :: Members '[Reader TyDefCtx, Error LocTCError] r => ModuleName -> TypeDefn -> Sem r ()
checkTyDefn :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error LocTCError] r =>
ModuleName -> TypeDefn -> Sem r ()
checkTyDefn ModuleName
name defn :: TypeDefn
defn@(TypeDefn String
x [String]
args Type
body) = forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError (Maybe (QName Term) -> TCError -> LocTCError
LocTCError (forall a. a -> Maybe a
Just (ModuleName
name forall a. ModuleName -> Name a -> QName a
.- forall a. String -> Name a
string2Name String
x))) forall a b. (a -> b) -> a -> b
$ do
  -- First, make sure the body is a valid type, i.e. everything inside
  -- it is well-kinded.
  forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
body

  -- Now make sure it is not directly cyclic (i.e. ensure it is a
  -- "productive" definition).
  Set String
_ <- forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy (String -> [Type] -> Type
TyUser String
x (forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Name a
string2Name) [String]
args)) forall a. Set a
S.empty

  -- Make sure it does not use any unbound type variables or undefined
  -- types.
  forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
TypeDefn -> Sem r ()
checkUnboundVars TypeDefn
defn

  -- Make sure it does not use any polymorphic recursion (polymorphic
  -- recursion isn't allowed at the moment since it can make the
  -- subtyping checker diverge).
  forall (r :: EffectRow).
Member (Error TCError) r =>
TypeDefn -> Sem r ()
checkPolyRec TypeDefn
defn

-- | Check if a given type is cyclic. A type 'ty' is cyclic if:
--
--   1. 'ty' is the name of a user-defined type.
--   2. Repeated expansions of the type yield nothing but other user-defined types.
--   3. An expansion of one of those types yields another type that has
--      been previously encountered.
--
--   In other words, repeatedly expanding the definition can get us
--   back to exactly where we started.
--
--   The function returns the set of TyDefs encountered during
--   expansion if the TyDef is not cyclic.
checkCyclicTy :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Set String -> Sem r (Set String)
checkCyclicTy :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy (TyUser String
name [Type]
args) Set String
set = do
  case forall a. Ord a => a -> Set a -> Bool
S.member String
name Set String
set of
    Bool
True -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ String -> TCError
CyclicTyDef String
name
    Bool
False -> do
      Type
ty <- forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args
      forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy Type
ty (forall a. Ord a => a -> Set a -> Set a
S.insert String
name Set String
set)
checkCyclicTy Type
_ Set String
set = forall (m :: * -> *) a. Monad m => a -> m a
return Set String
set

-- | Ensure that a type definition does not use any unbound type
--   variables or undefined types.
checkUnboundVars :: Members '[Reader TyDefCtx, Error TCError] r => TypeDefn -> Sem r ()
checkUnboundVars :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
TypeDefn -> Sem r ()
checkUnboundVars (TypeDefn String
_ [String]
args Type
body) = Type -> Sem r ()
go Type
body
 where
  go :: Type -> Sem r ()
go (TyAtom (AVar (U Name Type
x)))
    | forall a. Name a -> String
name2String Name Type
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Name Type -> TCError
UnboundTyVar Name Type
x
  go (TyAtom Atom
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  go (TyUser String
name [Type]
tys) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
tys forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Sem r ()
go [Type]
tys
  go (TyCon Con
_ [Type]
tys) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Sem r ()
go [Type]
tys

-- | Check for polymorphic recursion: starting from a user-defined
--   type, keep expanding its definition recursively, ensuring that
--   any recursive references to the defined type have only type variables
--   as arguments.
checkPolyRec :: Member (Error TCError) r => TypeDefn -> Sem r ()
checkPolyRec :: forall (r :: EffectRow).
Member (Error TCError) r =>
TypeDefn -> Sem r ()
checkPolyRec (TypeDefn String
name [String]
args Type
body) = Type -> Sem r ()
go Type
body
 where
  go :: Type -> Sem r ()
go (TyCon (CUser String
x) [Type]
tys)
    | String
x forall a. Eq a => a -> a -> Bool
== String
name Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTyVar [Type]
tys) =
        forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ String -> [String] -> [Type] -> TCError
NoPolyRec String
name [String]
args [Type]
tys
    | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  go (TyCon Con
_ [Type]
tys) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Sem r ()
go [Type]
tys
  go Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Keep only the duplicate elements from a list.
--
--   >>> filterDups [1,3,2,1,1,4,2]
--   [1,2]
filterDups :: Ord a => [a] -> [a]
filterDups :: forall a. Ord a => [a] -> [a]
filterDups = forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
> Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [[a]]
group forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort

--------------------------------------------------
-- Type declarations

-- | Given a list of type declarations from a module, first check that
--   there are no duplicate type declarations, and that the types are
--   well-formed; then create a type context containing the given
--   declarations.
makeTyCtx :: Members '[Reader TyDefCtx, Error TCError] r => ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx ModuleName
name [TypeDecl]
decls = do
  let dups :: [Name Term]
dups = forall a. Ord a => [a] -> [a]
filterDups forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(TypeDecl Name Term
x PolyType
_) -> Name Term
x) forall a b. (a -> b) -> a -> b
$ [TypeDecl]
decls
  case [Name Term]
dups of
    (Name Term
x : [Name Term]
_) -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
DuplicateDecls Name Term
x)
    [] -> do
      forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
TyCtx -> Sem r ()
checkCtx TyCtx
declCtx
      forall (m :: * -> *) a. Monad m => a -> m a
return TyCtx
declCtx
 where
  declCtx :: TyCtx
declCtx = forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(TypeDecl Name Term
x PolyType
ty) -> (Name Term
x, PolyType
ty)) [TypeDecl]
decls

-- | Check that all the types in a context are valid.
checkCtx :: Members '[Reader TyDefCtx, Error TCError] r => TyCtx -> Sem r ()
checkCtx :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
TyCtx -> Sem r ()
checkCtx = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Ctx a b -> [b]
Ctx.elems

--------------------------------------------------
-- Top-level definitions

-- | Type check a top-level definition in the given module.
checkDefn ::
  Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output (Message ann)] r =>
  ModuleName ->
  TermDefn ->
  Sem r Defn
checkDefn :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh,
    Output (Message ann)]
  r =>
ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name (TermDefn Name Term
x [Bind [Pattern] Term]
clauses) = forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError (Maybe (QName Term) -> TCError -> LocTCError
LocTCError (forall a. a -> Maybe a
Just (ModuleName
name forall a. ModuleName -> Name a -> QName a
.- Name Term
x))) forall a b. (a -> b) -> a -> b
$ do
  -- Check that all clauses have the same number of patterns
  [Bind [Pattern] Term] -> Sem (Error TCError : r) ()
checkNumPats [Bind [Pattern] Term]
clauses

  -- Get the declared type signature of x
  Forall Bind [Name Type] Type
sig <- forall a b (r :: EffectRow).
Member (Reader (Ctx a b)) r =>
QName a -> Sem r (Maybe b)
lookup (ModuleName
name forall a. ModuleName -> Name a -> QName a
.- Name Term
x) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Name Term -> TCError
NoType Name Term
x) forall (m :: * -> *) a. Monad m => a -> m a
return
  -- If x isn't in the context, it's because no type was declared for it, so
  -- throw an error.
  ([Name Type]
nms, Type
ty) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Type
sig

  -- Try to decompose the type into a chain of arrows like pty1 ->
  -- pty2 -> pty3 -> ... -> bodyTy, according to the number of
  -- patterns, and lazily unrolling type definitions along the way.
  ([Type]
patTys, Type
bodyTy) <- forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Bind [Pattern] Term -> Int
numPats (forall a. [a] -> a
head [Bind [Pattern] Term]
clauses)) Type
ty

  (([Clause]
acs, Type
_), S
theta) <- forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve forall a b. (a -> b) -> a -> b
$ do
    [Clause]
aclauses <- forall (r :: EffectRow) a.
Member (Writer Constraint) r =>
[Name Type] -> Sem r a -> Sem r a
forAll [Name Type]
nms forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Type] -> Type -> Bind [Pattern] Term -> Sem r Clause
checkClause [Type]
patTys Type
bodyTy) [Bind [Pattern] Term]
clauses
    forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
aclauses, Type
ty)

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. Subst b a => Substitution b -> a -> a
applySubst S
theta (Name ATerm -> [Type] -> Type -> [Clause] -> Defn
Defn (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x) [Type]
patTys Type
bodyTy [Clause]
acs)
 where
  numPats :: Bind [Pattern] Term -> Int
numPats = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind

  checkNumPats :: [Bind [Pattern] Term] -> Sem (Error TCError : r) ()
checkNumPats [] = forall (m :: * -> *) a. Monad m => a -> m a
return () -- This can't happen, but meh
  checkNumPats [Bind [Pattern] Term
_] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  checkNumPats (Bind [Pattern] Term
c : [Bind [Pattern] Term]
cs)
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
== Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term -> Int
numPats) (Bind [Pattern] Term
c forall a. a -> [a] -> [a]
: [Bind [Pattern] Term]
cs) = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
DuplicateDefns Name Term
x)
    | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
== Bind [Pattern] Term -> Int
numPats Bind [Pattern] Term
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term -> Int
numPats) [Bind [Pattern] Term]
cs) = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw TCError
NumPatterns
    -- XXX more info, this error actually means # of
    -- patterns don't match across different clauses
    | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- \| Check a clause of a definition against a list of pattern types and a body type.
  checkClause ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    [Type] ->
    Type ->
    Bind [Pattern] Term ->
    Sem r Clause
  checkClause :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Type] -> Type -> Bind [Pattern] Term -> Sem r Clause
checkClause [Type]
patTys Type
bodyTy Bind [Pattern] Term
clause = do
    ([Pattern]
pats, Term
body) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Pattern] Term
clause

    -- At this point we know that every clause has the same number of patterns,
    -- which is the same as the length of the list patTys.  So we can just use
    -- zipWithM to check all the patterns.
    ([TyCtx]
ctxs, [APattern]
aps) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern [Pattern]
pats [Type]
patTys
    ATerm
at <- forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends (forall a. Monoid a => [a] -> a
mconcat [TyCtx]
ctxs) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
body Type
bodyTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [APattern]
aps ATerm
at

  -- Decompose a type that must be of the form t1 -> t2 -> ... -> tn -> t{n+1}.
  decomposeDefnTy :: Members '[Reader TyDefCtx, Error TCError] r => Int -> Type -> Sem r ([Type], Type)
  decomposeDefnTy :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
0 Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
ty)
  decomposeDefnTy Int
n (TyUser String
tyName [Type]
args) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
tyName [Type]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
n
  decomposeDefnTy Int
n (Type
ty1 :->: Type
ty2) = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type
ty1 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Int
n forall a. Num a => a -> a -> a
- Int
1) Type
ty2
  decomposeDefnTy Int
_n Type
_ty = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw TCError
NumPatterns

-- XXX include more info. More argument patterns than arrows in the type.

--------------------------------------------------
-- Properties

-- | Given a context mapping names to documentation, extract the
--   properties attached to each name and typecheck them.
checkProperties ::
  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r =>
  Ctx Term Docs ->
  Sem r (Ctx ATerm [AProperty])
checkProperties :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docs =
  forall a1 b a2. Ctx a1 b -> Ctx a2 b
Ctx.coerceKeys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. (b -> Bool) -> Ctx a b -> Ctx a b
Ctx.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Term -> Sem r ATerm
checkProperty Ctx Term [Term]
properties
 where
  properties :: Ctx Term [Property]
  properties :: Ctx Term [Term]
properties = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Docs
ds -> [Term
p | DocProperty Term
p <- Docs
ds]) Ctx Term Docs
docs

-- | Check the types of the terms embedded in a property.
checkProperty ::
  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r =>
  Property ->
  Sem r AProperty
checkProperty :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Term -> Sem r ATerm
checkProperty Term
prop = do
  (ATerm
at, S
theta) <- forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
prop Type
TyProp
  -- XXX do we need to default container variables here?
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. Subst b a => Substitution b -> a -> a
applySubst S
theta ATerm
at

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

--------------------------------------------------
-- Checking types/kinds
--------------------------------------------------

-- | Check that a sigma type is a valid type.  See 'checkTypeValid'.
checkPolyTyValid :: Members '[Reader TyDefCtx, Error TCError] r => PolyType -> Sem r ()
checkPolyTyValid :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid (Forall Bind [Name Type] Type
b) = do
  let ([Name Type]
_, Type
ty) = forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind Bind [Name Type] Type
b
  forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
ty

-- | Disco doesn't need kinds per se, since all types must be fully
--   applied.  But we do need to check that every type is applied to
--   the correct number of arguments.
checkTypeValid :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Sem r ()
checkTypeValid :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid (TyAtom Atom
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkTypeValid (TyCon Con
c [Type]
tys) = do
  Int
k <- forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Con -> Sem r Int
conArity Con
c
  if
    | Int
n forall a. Ord a => a -> a -> Bool
< Int
k -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> TCError
NotEnoughArgs Con
c)
    | Int
n forall a. Ord a => a -> a -> Bool
> Int
k -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> TCError
TooManyArgs Con
c)
    | Bool
otherwise -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid [Type]
tys
 where
  n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys

conArity :: Members '[Reader TyDefCtx, Error TCError] r => Con -> Sem r Int
conArity :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Con -> Sem r Int
conArity (CContainer Atom
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity Con
CGraph = forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity (CUser String
name) = do
  TyDefCtx
d <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name TyDefCtx
d of
    Maybe TyDefBody
Nothing -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> TCError
NotTyDef String
name)
    Just (TyDefBody [String]
as [Type] -> Type
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
as)
conArity Con
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Int
2 -- (->, *, +, map)

--------------------------------------------------
-- Checking modes
--------------------------------------------------

-- | Typechecking can be in one of two modes: inference mode means we
--   are trying to synthesize a valid type for a term; checking mode
--   means we are trying to show that a term has a given type.
data Mode = Infer | Check Type
  deriving (Int -> Mode -> ShowS
[Mode] -> ShowS
Mode -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mode] -> ShowS
$cshowList :: [Mode] -> ShowS
show :: Mode -> String
$cshow :: Mode -> String
showsPrec :: Int -> Mode -> ShowS
$cshowsPrec :: Int -> Mode -> ShowS
Show)

-- | Check that a term has the given type.  Either throws an error, or
--   returns the term annotated with types for all subterms.
--
--   This function is provided for convenience; it simply calls
--   'typecheck' with an appropriate 'Mode'.
check ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Term ->
  Type ->
  Sem r ATerm
check :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty = forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck (Type -> Mode
Check Type
ty) Term
t

-- | Check that a term has the given polymorphic type.
checkPolyTy ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Term ->
  PolyType ->
  Sem r ATerm
checkPolyTy :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t (Forall Bind [Name Type] Type
sig) = do
  ([Name Type]
as, Type
tau) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Type
sig
  (ATerm
at, Constraint
cst) <- forall (r :: EffectRow) a.
Sem (Writer Constraint : r) a -> Sem r (a, Constraint)
withConstraint forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
tau
  case [Name Type]
as of
    [] -> forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint Constraint
cst
    [Name Type]
_ -> forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Bind [Name Type] Constraint -> Constraint
CAll (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Type]
as Constraint
cst)
  forall (m :: * -> *) a. Monad m => a -> m a
return ATerm
at

-- | Infer the type of a term.  If it succeeds, it returns the term
--   with all subterms annotated.
--
--   This function is provided for convenience; it simply calls
--   'typecheck' with an appropriate 'Mode'.
infer ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Term ->
  Sem r ATerm
infer :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer = forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
Infer

-- | Top-level type inference algorithm: infer a (polymorphic) type
--   for a term by running type inference, solving the resulting
--   constraints, and quantifying over any remaining type variables.
inferTop ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
  Term ->
  Sem r (ATerm, PolyType)
inferTop :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t = do
  -- Run inference on the term and try to solve the resulting
  -- constraints.
  (ATerm
at, S
theta) <- forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t

  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Final annotated term (before substitution and container monomorphizing):"
  forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty ATerm
at

  -- Apply the resulting substitution.
  let at' :: ATerm
at' = forall b a. Subst b a => Substitution b -> a -> a
applySubst S
theta ATerm
at

      -- Find any remaining container variables.
      cvs :: Set (Name Type)
cvs = Type -> Set (Name Type)
containerVars (forall t. HasType t => t -> Type
getType ATerm
at')

      -- Replace them all with List.
      at'' :: ATerm
at'' = forall b a. Subst b a => Substitution b -> a -> a
applySubst (forall a. [(Name a, a)] -> Substitution a
Subst.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Set a -> [a]
S.toList Set (Name Type)
cvs) (forall a. a -> [a]
repeat (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrList)))) ATerm
at'

  -- Finally, quantify over any remaining type variables and return
  -- the term along with the resulting polymorphic type.
  forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm
at'', Type -> PolyType
closeType (forall t. HasType t => t -> Type
getType ATerm
at''))

-- | Top-level type checking algorithm: check that a term has a given
--   polymorphic type by running type checking and solving the
--   resulting constraints.
checkTop ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
  Term ->
  PolyType ->
  Sem r ATerm
checkTop :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkTop Term
t PolyType
ty = do
  (ATerm
at, S
theta) <- forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t PolyType
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. Subst b a => Substitution b -> a -> a
applySubst S
theta ATerm
at

--------------------------------------------------
-- The typecheck function
--------------------------------------------------

-- | The main workhorse of the typechecker.  Instead of having two
--   functions, one for inference and one for checking, 'typecheck'
--   takes a 'Mode'.  This cuts down on code duplication in many
--   cases, and allows all the checking and inference code related to
--   a given AST node to be placed together.
typecheck ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Mode ->
  Term ->
  Sem r ATerm
-- ~~~~ Note [Pattern coverage]
-- In several places we have clauses like
--
--   inferPrim (PrimBOp op) | op `elem` [And, Or, Impl, Iff]
--
-- since the typing rules for all the given operators are the same.
-- The only problem is that the pattern coverage checker (sensibly)
-- doesn't look at guards in general, so it thinks that there are TBin
-- cases still uncovered.
--
-- However, we *don't* just want to add a catch-all case at the end,
-- because the coverage checker is super helpful in alerting us when
-- there's a missing typechecking case after modifying the language in
-- some way. The (not ideal) solution for now is to add some
-- additional explicit cases that simply call 'error', which will
-- never be reached but which assure the coverage checker that we have
-- handled those cases.
--
-- The ideal solution would be to use or-patterns, if Haskell had them
-- (see https://github.com/ghc-proposals/ghc-proposals/pull/43).

--------------------------------------------------
-- Defined types

-- To check at a user-defined type, expand its definition and recurse.
-- This case has to be first, so in all other cases we know the type
-- will not be a TyUser.
typecheck :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck (Check (TyUser String
name [Type]
args)) Term
t = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t
--------------------------------------------------
-- Parens

-- Recurse through parens; they are not represented explicitly in the
-- resulting ATerm.
typecheck Mode
mode (TParens Term
t) = forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t
--------------------------------------------------
-- Variables

-- Resolve variable names and infer their types.  We don't need a
-- checking case; checking the type of a variable will fall through to
-- this case.
typecheck Mode
Infer (TVar Name Term
x) = do
  -- Pick the first method that succeeds; if none do, throw an unbound
  -- variable error.
  Maybe ATerm
mt <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ [Sem r (Maybe ATerm)
tryLocal, Sem r (Maybe ATerm)
tryModule, Sem r (Maybe ATerm)
tryPrim]
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
Unbound Name Term
x)) forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ATerm
mt
 where
  -- 1. See if the variable name is bound locally.
  tryLocal :: Sem r (Maybe ATerm)
tryLocal = do
    Maybe PolyType
mty <- forall a b (r :: EffectRow).
Member (Reader (Ctx a b)) r =>
QName a -> Sem r (Maybe b)
Ctx.lookup (forall a. Name a -> QName a
localName Name Term
x)
    case Maybe PolyType
mty of
      Just (Forall Bind [Name Type] Type
sig) -> do
        ([Name Type]
_, Type
ty) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Type
sig
        forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Type -> QName ATerm -> ATerm
ATVar Type
ty (forall a. Name a -> QName a
localName (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x))
      Maybe PolyType
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

  -- 2. See if the variable name is bound in some in-scope module,
  -- throwing an ambiguity error if it is bound in multiple modules.
  tryModule :: Sem r (Maybe ATerm)
tryModule = do
    [(ModuleName, PolyType)]
bs <- forall a b (r :: EffectRow).
Member (Reader (Ctx a b)) r =>
Name a -> Sem r [(ModuleName, b)]
Ctx.lookupNonLocal Name Term
x
    case [(ModuleName, PolyType)]
bs of
      [(ModuleName
m, Forall Bind [Name Type] Type
sig)] -> do
        ([Name Type]
_, Type
ty) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Type] Type
sig
        forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Type -> QName ATerm -> ATerm
ATVar Type
ty (ModuleName
m forall a. ModuleName -> Name a -> QName a
.- coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x)
      [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      [(ModuleName, PolyType)]
_ -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Name Term -> [ModuleName] -> TCError
Ambiguous Name Term
x (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(ModuleName, PolyType)]
bs)

  -- 3. See if we should convert it to a primitive.
  tryPrim :: Sem r (Maybe ATerm)
tryPrim =
    case String -> [Prim]
toPrim (forall a. Name a -> String
name2String Name Term
x) of
      (Prim
prim : [Prim]
_) -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
Infer (Prim -> Term
TPrim Prim
prim)
      [Prim]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

--------------------------------------------------
-- Primitives

typecheck Mode
Infer (TPrim Prim
prim) = do
  Type
ty <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Prim -> Sem r Type
inferPrim Prim
prim
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Prim -> ATerm
ATPrim Type
ty Prim
prim
 where
  inferPrim :: Members '[Writer Constraint, Fresh] r => Prim -> Sem r Type

  ----------------------------------------
  -- Left/right

  inferPrim :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Prim -> Sem r Type
inferPrim Prim
PrimLeft = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:->: (Type
a Type -> Type -> Type
:+: Type
b)
  inferPrim Prim
PrimRight = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
b Type -> Type -> Type
:->: (Type
a Type -> Type -> Type
:+: Type
b)

  ----------------------------------------
  -- Logic

  inferPrim (PrimBOp BOp
op) | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
And, BOp
Or, BOp
Impl, BOp
Iff] = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual (BOp -> Qualifier
bopQual BOp
op) Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
a

  -- See Note [Pattern coverage] -----------------------------
  inferPrim (PrimBOp BOp
And) = forall a. HasCallStack => String -> a
error String
"inferPrim And should be unreachable"
  inferPrim (PrimBOp BOp
Or) = forall a. HasCallStack => String -> a
error String
"inferPrim Or should be unreachable"
  inferPrim (PrimBOp BOp
Impl) = forall a. HasCallStack => String -> a
error String
"inferPrim Impl should be unreachable"
  inferPrim (PrimBOp BOp
Iff) = forall a. HasCallStack => String -> a
error String
"inferPrim Iff should be unreachable"
  ------------------------------------------------------------

  inferPrim (PrimUOp UOp
Not) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QBool Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:->: Type
a

  ----------------------------------------
  -- Container conversion

  inferPrim Prim
conv | Prim
conv forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimList, Prim
PrimBag, Prim
PrimSet] = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom -- make a unification variable for the container type
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy -- make a unification variable for the element type

    -- converting to a set or bag requires being able to sort the elements
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Prim
conv forall a. Eq a => a -> a -> Bool
/= Prim
PrimList) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Prim -> Type -> Type
primCtrCon Prim
conv Type
a
   where
    primCtrCon :: Prim -> Type -> Type
primCtrCon Prim
PrimList = Type -> Type
TyList
    primCtrCon Prim
PrimBag = Type -> Type
TyBag
    primCtrCon Prim
_ = Type -> Type
TySet

  -- See Note [Pattern coverage] -----------------------------
  inferPrim Prim
PrimList = forall a. HasCallStack => String -> a
error String
"inferPrim PrimList should be unreachable"
  inferPrim Prim
PrimBag = forall a. HasCallStack => String -> a
error String
"inferPrim PrimBag should be unreachable"
  inferPrim Prim
PrimSet = forall a. HasCallStack => String -> a
error String
"inferPrim PrimSet should be unreachable"
  ------------------------------------------------------------

  inferPrim Prim
PrimB2C = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyBag Type
a Type -> Type -> Type
:->: Type -> Type
TySet (Type
a Type -> Type -> Type
:*: Type
TyN)
  inferPrim Prim
PrimC2B = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c (Type
a Type -> Type -> Type
:*: Type
TyN) Type -> Type -> Type
:->: Type -> Type
TyBag Type
a
  inferPrim Prim
PrimUC2B = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c (Type
a Type -> Type -> Type
:*: Type
TyN) Type -> Type -> Type
:->: Type -> Type
TyBag Type
a
  inferPrim Prim
PrimMapToSet = do
    Type
k <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
v <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
k
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TyMap Type
k Type
v Type -> Type -> Type
:->: Type -> Type
TySet (Type
k Type -> Type -> Type
:*: Type
v)
  inferPrim Prim
PrimSetToMap = do
    Type
k <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
v <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
k
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TySet (Type
k Type -> Type -> Type
:*: Type
v) Type -> Type -> Type
:->: Type -> Type -> Type
TyMap Type
k Type
v
  inferPrim Prim
PrimSummary = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyGraph Type
a Type -> Type -> Type
:->: Type -> Type -> Type
TyMap Type
a (Type -> Type
TySet Type
a)
  inferPrim Prim
PrimVertex = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:->: Type -> Type
TyGraph Type
a
  inferPrim Prim
PrimEmptyGraph = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyGraph Type
a
  inferPrim Prim
PrimOverlay = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyGraph Type
a Type -> Type -> Type
:*: Type -> Type
TyGraph Type
a Type -> Type -> Type
:->: Type -> Type
TyGraph Type
a
  inferPrim Prim
PrimConnect = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyGraph Type
a Type -> Type -> Type
:*: Type -> Type
TyGraph Type
a Type -> Type -> Type
:->: Type -> Type
TyGraph Type
a
  inferPrim Prim
PrimInsert = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
b Type -> Type -> Type
:*: Type -> Type -> Type
TyMap Type
a Type
b Type -> Type -> Type
:->: Type -> Type -> Type
TyMap Type
a Type
b
  inferPrim Prim
PrimLookup = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type -> Type -> Type
TyMap Type
a Type
b Type -> Type -> Type
:->: (Type
TyUnit Type -> Type -> Type
:+: Type
b)
  ----------------------------------------
  -- Container primitives

  inferPrim (PrimBOp BOp
Cons) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type -> Type
TyList Type
a Type -> Type -> Type
:->: Type -> Type
TyList Type
a

  -- XXX see https://github.com/disco-lang/disco/issues/160
  -- each : (a -> b) × c a -> c b
  inferPrim Prim
PrimEach = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Type
a Type -> Type -> Type
:->: Type
b) Type -> Type -> Type
:*: Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Atom -> Type -> Type
TyContainer Atom
c Type
b

  -- XXX should eventually be (a * a -> a) * c a -> a,
  --   with a check that the function has the right properties.
  -- reduce : (a * a -> a) * a * c a -> a
  inferPrim Prim
PrimReduce = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
a) Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:*: Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Type
a

  -- filter : (a -> Bool) × c a -> c a
  inferPrim Prim
PrimFilter = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Type
a Type -> Type -> Type
:->: Type
TyBool) Type -> Type -> Type
:*: Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Atom -> Type -> Type
TyContainer Atom
c Type
a

  -- join : c (c a) -> c a
  inferPrim Prim
PrimJoin = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c (Atom -> Type -> Type
TyContainer Atom
c Type
a) Type -> Type -> Type
:->: Atom -> Type -> Type
TyContainer Atom
c Type
a

  -- merge : (N × N -> N) × c a × c a -> c a   (c = bag or set)
  inferPrim Prim
PrimMerge = do
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
      [Constraint] -> Constraint
COr
        [ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrBag)) (Atom -> Type
TyAtom Atom
c)
        , Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrSet)) (Atom -> Type
TyAtom Atom
c)
        ]
    let ca :: Type
ca = Atom -> Type -> Type
TyContainer Atom
c Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Type
TyN Type -> Type -> Type
:*: Type
TyN Type -> Type -> Type
:->: Type
TyN) Type -> Type -> Type
:*: Type
ca Type -> Type -> Type
:*: Type
ca Type -> Type -> Type
:->: Type
ca
  inferPrim (PrimBOp BOp
CartProd) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:*: Atom -> Type -> Type
TyContainer Atom
c Type
b Type -> Type -> Type
:->: Atom -> Type -> Type
TyContainer Atom
c (Type
a Type -> Type -> Type
:*: Type
b)
  inferPrim (PrimBOp BOp
setOp) | BOp
setOp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Union, BOp
Inter, BOp
Diff, BOp
Subset] = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
      [Constraint] -> Constraint
COr
        [ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrBag)) (Atom -> Type
TyAtom Atom
c)
        , Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrSet)) (Atom -> Type
TyAtom Atom
c)
        ]
    let ca :: Type
ca = Atom -> Type -> Type
TyContainer Atom
c Type
a
    let resTy :: Type
resTy = case BOp
setOp of BOp
Subset -> Type
TyBool; BOp
_ -> Type
ca
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
ca Type -> Type -> Type
:*: Type
ca Type -> Type -> Type
:->: Type
resTy

  -- See Note [Pattern coverage] -----------------------------
  inferPrim (PrimBOp BOp
Union) = forall a. HasCallStack => String -> a
error String
"inferPrim Union should be unreachable"
  inferPrim (PrimBOp BOp
Inter) = forall a. HasCallStack => String -> a
error String
"inferPrim Inter should be unreachable"
  inferPrim (PrimBOp BOp
Diff) = forall a. HasCallStack => String -> a
error String
"inferPrim Diff should be unreachable"
  inferPrim (PrimBOp BOp
Subset) = forall a. HasCallStack => String -> a
error String
"inferPrim Subset should be unreachable"
  ------------------------------------------------------------

  inferPrim (PrimBOp BOp
Elem) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom

    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Type
TyBool

  ----------------------------------------
  -- Arithmetic

  inferPrim (PrimBOp BOp
IDiv) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
resTy <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
resTy
  inferPrim (PrimBOp BOp
Mod) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
a Type
TyZ
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
a
  inferPrim (PrimBOp BOp
op) | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Add, BOp
Mul, BOp
Sub, BOp
Div, BOp
SSub] = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual (BOp -> Qualifier
bopQual BOp
op) Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
a

  -- See Note [Pattern coverage] -----------------------------
  inferPrim (PrimBOp BOp
Add) = forall a. HasCallStack => String -> a
error String
"inferPrim Add should be unreachable"
  inferPrim (PrimBOp BOp
Mul) = forall a. HasCallStack => String -> a
error String
"inferPrim Mul should be unreachable"
  inferPrim (PrimBOp BOp
Sub) = forall a. HasCallStack => String -> a
error String
"inferPrim Sub should be unreachable"
  inferPrim (PrimBOp BOp
Div) = forall a. HasCallStack => String -> a
error String
"inferPrim Div should be unreachable"
  inferPrim (PrimBOp BOp
SSub) = forall a. HasCallStack => String -> a
error String
"inferPrim SSub should be unreachable"
  ------------------------------------------------------------

  inferPrim (PrimUOp UOp
Neg) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSub Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:->: Type
a
  inferPrim (PrimBOp BOp
Exp) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
resTy <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r Type
cExp Type
a Type
b
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
b Type -> Type -> Type
:->: Type
resTy

  ----------------------------------------
  -- Number theory

  inferPrim Prim
PrimIsPrime = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyBool
  inferPrim Prim
PrimFactor = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type -> Type
TyBag Type
TyN
  inferPrim Prim
PrimFrac = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyQ Type -> Type -> Type
:->: (Type
TyZ Type -> Type -> Type
:*: Type
TyN)
  inferPrim (PrimBOp BOp
Divides) = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:*: Type
a Type -> Type -> Type
:->: Type
TyBool

  ----------------------------------------
  -- Choose

  -- For now, a simple typing rule for multinomial coefficients that
  -- requires everything to be Nat.  However, they can be extended to
  -- handle negative or fractional arguments.
  inferPrim (PrimBOp BOp
Choose) = do
    Type
b <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy

    -- b can be either Nat (a binomial coefficient)
    -- or a list of Nat (a multinomial coefficient).
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ [Constraint] -> Constraint
COr [Type -> Type -> Constraint
CEq Type
b Type
TyN, Type -> Type -> Constraint
CEq Type
b (Type -> Type
TyList Type
TyN)]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:*: Type
b Type -> Type -> Type
:->: Type
TyN

  ----------------------------------------
  -- Ellipses

  -- Actually 'until' supports more types than this, e.g. Q instead
  -- of N, but this is good enough.  This case is here just for
  -- completeness---in case someone enables primitives and uses it
  -- directly---but typically 'until' is generated only during
  -- desugaring of a container with ellipsis, after typechecking, in
  -- which case it can be assigned a more appropriate type directly.

  inferPrim Prim
PrimUntil = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:*: Type -> Type
TyList Type
TyN Type -> Type -> Type
:->: Type -> Type
TyList Type
TyN
  ----------------------------------------
  -- Crash

  inferPrim Prim
PrimCrash = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyString Type -> Type -> Type
:->: Type
a

  ----------------------------------------
  -- Propositions

  -- 'holds' converts a Prop into a Bool (but might not terminate).
  inferPrim Prim
PrimHolds = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyProp Type -> Type -> Type
:->: Type
TyBool
  -- An equality assertion =!= is just like a comparison ==, except
  -- the result is a Prop.
  inferPrim (PrimBOp BOp
ShouldEq) = do
    Type
ty <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
TyProp
  inferPrim (PrimBOp BOp
ShouldLt) = do
    Type
ty <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
TyProp

  ----------------------------------------
  -- Comparisons

  -- Infer the type of a comparison. A comparison always has type
  -- Bool, but we have to make sure the subterms have compatible
  -- types.  We also generate a QCmp qualifier, for two reasons:
  -- one, we need to know whether e.g. a comparison was done at a
  -- certain type, so we can decide whether the type is allowed to
  -- be completely polymorphic or not.  Also, comparison of Props is
  -- not allowed.
  inferPrim (PrimBOp BOp
op) | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Eq, BOp
Neq, BOp
Lt, BOp
Gt, BOp
Leq, BOp
Geq] = do
    Type
ty <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
TyBool

  -- See Note [Pattern coverage] -----------------------------
  inferPrim (PrimBOp BOp
Eq) = forall a. HasCallStack => String -> a
error String
"inferPrim Eq should be unreachable"
  inferPrim (PrimBOp BOp
Neq) = forall a. HasCallStack => String -> a
error String
"inferPrim Neq should be unreachable"
  inferPrim (PrimBOp BOp
Lt) = forall a. HasCallStack => String -> a
error String
"inferPrim Lt should be unreachable"
  inferPrim (PrimBOp BOp
Gt) = forall a. HasCallStack => String -> a
error String
"inferPrim Gt should be unreachable"
  inferPrim (PrimBOp BOp
Leq) = forall a. HasCallStack => String -> a
error String
"inferPrim Leq should be unreachable"
  inferPrim (PrimBOp BOp
Geq) = forall a. HasCallStack => String -> a
error String
"inferPrim Geq should be unreachable"
  ------------------------------------------------------------

  inferPrim (PrimBOp BOp
op) | BOp
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Min, BOp
Max] = do
    Type
ty <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
ty Type -> Type -> Type
:*: Type
ty Type -> Type -> Type
:->: Type
ty

  -- See Note [Pattern coverage] -----------------------------
  inferPrim (PrimBOp BOp
Min) = forall a. HasCallStack => String -> a
error String
"inferPrim Min should be unreachable"
  inferPrim (PrimBOp BOp
Max) = forall a. HasCallStack => String -> a
error String
"inferPrim Max should be unreachable"
  ------------------------------------------------------------

  ----------------------------------------
  -- Special arithmetic functions: fact, sqrt, floor, ceil, abs

  inferPrim (PrimUOp UOp
Fact) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyN
  inferPrim Prim
PrimSqrt = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyN
  inferPrim Prim
p | Prim
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimFloor, Prim
PrimCeil] = do
    Type
argTy <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
resTy <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
argTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
argTy Type -> Type -> Type
:->: Type
resTy

  -- See Note [Pattern coverage] -----------------------------
  inferPrim Prim
PrimFloor = forall a. HasCallStack => String -> a
error String
"inferPrim Floor should be unreachable"
  inferPrim Prim
PrimCeil = forall a. HasCallStack => String -> a
error String
"inferPrim Ceil should be unreachable"
  ------------------------------------------------------------

  inferPrim Prim
PrimAbs = do
    Type
argTy <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Type
resTy <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r ()
cAbs Type
argTy Type
resTy forall (r :: EffectRow).
Members '[Writer Constraint] r =>
Sem r () -> Sem r () -> Sem r ()
`cOr` forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r ()
cSize Type
argTy Type
resTy
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
argTy Type -> Type -> Type
:->: Type
resTy

  ----------------------------------------
  -- power set/bag

  inferPrim Prim
PrimPower = do
    Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
    Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom

    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
      [Constraint] -> Constraint
COr
        [ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrSet)) (Atom -> Type
TyAtom Atom
c)
        , Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom (BaseTy -> Atom
ABase BaseTy
CtrBag)) (Atom -> Type
TyAtom Atom
c)
        ]

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type -> Type
TyContainer Atom
c Type
a Type -> Type -> Type
:->: Atom -> Type -> Type
TyContainer Atom
c (Atom -> Type -> Type
TyContainer Atom
c Type
a)
  inferPrim Prim
PrimLookupSeq = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyList Type
TyN Type -> Type -> Type
:->: (Type
TyUnit Type -> Type -> Type
:+: Type
TyString)
  inferPrim Prim
PrimExtendSeq = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Type
TyList Type
TyN Type -> Type -> Type
:->: Type -> Type
TyList Type
TyN

--------------------------------------------------
-- Base types

-- A few trivial cases for base types.
typecheck Mode
Infer Term
TUnit = forall (m :: * -> *) a. Monad m => a -> m a
return ATerm
ATUnit
typecheck Mode
Infer (TBool Bool
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Bool -> ATerm
ATBool Type
TyBool Bool
b
typecheck Mode
Infer (TChar Char
c) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Char -> ATerm
ATChar Char
c
typecheck Mode
Infer (TString String
cs) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> ATerm
ATString String
cs
-- typecheck (Check (TyFin n)) (TNat x)     = return $ ATNat (TyFin n) x
typecheck Mode
Infer (TNat Integer
n) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Integer -> ATerm
ATNat Type
TyN Integer
n
typecheck Mode
Infer (TRat Rational
r) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Rational -> ATerm
ATRat Rational
r
typecheck Mode
_ Term
TWild = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw TCError
NoTWild
--------------------------------------------------
-- Abstractions (lambdas and quantifiers)

-- Lambdas and quantifiers are similar enough that we can share a
-- bunch of the code, but their typing rules are a bit different.  In
-- particular a lambda
--
--   \(x1:ty1), (x2:ty2) ... . body
--
-- is going to have a type like ty1 -> ty2 -> ... -> resTy, whereas a
-- quantifier like
--
--   ∃(x1:ty1), (x2:ty2) ... . body
--
-- is just going to have the type Prop.  The similarity is that in
-- both cases we have to generate unification variables for any
-- binders with omitted type annotations, and typecheck the body under
-- an extended context.

-- It's only helpful to do lambdas in checking mode, since the
-- provided function type can provide information about the types of
-- the arguments.  For other quantifiers we can just fall back to
-- inference mode.
typecheck (Check Type
checkTy) tm :: Term
tm@(TAbs Quantifier
Lam Bind [Pattern] Term
body) = do
  ([Pattern]
args, Term
t) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Pattern] Term
body

  -- First check that the given type is of the form ty1 -> ty2 ->
  -- ... -> resTy, where the types ty1, ty2 ... match up with any
  -- types declared for the arguments to the lambda (e.g.  (x:tyA)
  -- (y:tyB) -> ...).
  (TyCtx
ctx, [APattern]
typedArgs, Type
resTy) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [Pattern]
args Type
checkTy Term
tm

  -- Then check the type of the body under a context extended with
  -- types for all the arguments.
  forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx forall a b. (a -> b) -> a -> b
$
    Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
Lam Type
checkTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (coerce :: forall a b. Coercible a b => a -> b
coerce [APattern]
typedArgs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
resTy)
 where
  -- Given the patterns and their optional type annotations in the
  -- head of a lambda (e.g.  @x (y:Z) (f : N -> N) -> ...@), and the
  -- type at which we are checking the lambda, ensure that:
  --
  --   - The type is of the form @ty1 -> ty2 -> ... -> resTy@ and
  --     there are enough @ty1@, @ty2@, ... to match all the arguments.
  --   - Each pattern successfully checks at its corresponding type.
  --
  -- If it succeeds, return a context binding variables to their
  -- types (as determined by the patterns and the input types) which
  -- we can use to extend when checking the body, a list of the typed
  -- patterns, and the result type of the function.
  checkArgs ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    [Pattern] ->
    Type ->
    Term ->
    Sem r (TyCtx, [APattern], Type)

  -- If we're all out of arguments, the remaining checking type is the
  -- result, and there are no variables to bind in the context.
  checkArgs :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [] Type
ty Term
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, [], Type
ty)
  -- Take the next pattern and its annotation; the checking type must
  -- be a function type ty1 -> ty2.
  checkArgs (Pattern
p : [Pattern]
args) Type
ty Term
term = do
    -- Ensure that ty is a function type
    (Type
ty1, Type
ty2) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CArr Type
ty (forall a b. a -> Either a b
Left Term
term)

    -- Check the argument pattern against the function domain.
    (TyCtx
pCtx, APattern
pTyped) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1

    -- Check the rest of the arguments under the type ty2, returning a
    -- context with the rest of the arguments and the final result type.
    (TyCtx
ctx, [APattern]
typedArgs, Type
resTy) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [Pattern]
args Type
ty2 Term
term

    -- Pass the result type through, and put the pattern-bound variables
    -- in the returned context.
    forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
pCtx forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx, APattern
pTyped forall a. a -> [a] -> [a]
: [APattern]
typedArgs, Type
resTy)

-- In inference mode, we handle lambdas as well as quantifiers (∀, ∃).
typecheck Mode
Infer (TAbs Quantifier
q Bind [Pattern] Term
lam) = do
  -- Open it and get the argument patterns with any type annotations.
  ([Pattern]
args, Term
t) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Pattern] Term
lam

  -- Replace any missing type annotations with fresh type variables,
  -- and check each pattern at that variable to refine them, collecting
  -- the types of each pattern's bound variables in a context.
  [Type]
tys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError, Fresh] r =>
Pattern -> Sem r Type
getAscrOrFresh [Pattern]
args
  ([TyCtx]
pCtxs, [APattern]
typedPats) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern [Pattern]
args [Type]
tys

  -- In the case of ∀, ∃, have to ensure that the argument types are
  -- searchable.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Quantifier
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier
All, Quantifier
Ex]) forall a b. (a -> b) -> a -> b
$
    -- What's the difference between this and `tys`? Nothing, after
    -- the solver runs, but right now the patterns might have a
    -- concrete type from annotations inside tuples.
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasType t => t -> Type
getType [APattern]
typedPats) forall a b. (a -> b) -> a -> b
$ \Type
ty ->
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
isSearchable Type
ty) forall a b. (a -> b) -> a -> b
$
        forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$
          Type -> TCError
NoSearch Type
ty

  -- Extend the context with the given arguments, and then do
  -- something appropriate depending on the quantifier.
  forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends (forall a. Monoid a => [a] -> a
mconcat [TyCtx]
pCtxs) forall a b. (a -> b) -> a -> b
$ do
    case Quantifier
q of
      -- For lambdas, infer the type of the body, and return an appropriate
      -- function type.
      Quantifier
Lam -> do
        ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
Lam ([Type] -> Type -> Type
mkFunTy [Type]
tys (forall t. HasType t => t -> Type
getType ATerm
at)) (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [APattern]
typedPats ATerm
at)

      -- For other quantifiers, check that the body has type Prop,
      -- and return Prop.
      Quantifier
_ -> do
        -- ∀, ∃
        ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
TyProp
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
q Type
TyProp (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [APattern]
typedPats ATerm
at)
 where
  getAscrOrFresh ::
    Members '[Reader TyDefCtx, Error TCError, Fresh] r =>
    Pattern ->
    Sem r Type
  getAscrOrFresh :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError, Fresh] r =>
Pattern -> Sem r Type
getAscrOrFresh (PAscr Pattern
_ Type
ty) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
ty forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
  getAscrOrFresh Pattern
_ = forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy

  -- mkFunTy [ty1, ..., tyn] out = ty1 -> (ty2 -> ... (tyn -> out))
  mkFunTy :: [Type] -> Type -> Type
  mkFunTy :: [Type] -> Type -> Type
mkFunTy [Type]
tys Type
out = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
out [Type]
tys

--------------------------------------------------
-- Application

-- Infer the type of a function application by inferring the function
-- type and then checking the argument type.  We don't need a checking
-- case because checking mode doesn't help.
typecheck Mode
Infer (TApp Term
t Term
t') = do
  ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
  let ty :: Type
ty = forall t. HasType t => t -> Type
getType ATerm
at
  (Type
ty1, Type
ty2) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CArr Type
ty (forall a b. a -> Either a b
Left Term
t)
  Type -> ATerm -> ATerm -> ATerm
ATApp Type
ty2 ATerm
at forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t' Type
ty1

--------------------------------------------------
-- Tuples

-- Check/infer the type of a tuple.
typecheck Mode
mode1 (TTup [Term]
tup) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> [ATerm] -> ATerm
ATTup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
mode1 [Term]
tup
 where
  typecheckTuple ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Mode ->
    [Term] ->
    Sem r (Type, [ATerm])
  typecheckTuple :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
_ [] = forall a. HasCallStack => String -> a
error String
"Impossible! typecheckTuple []"
  typecheckTuple Mode
mode [Term
t] = (forall t. HasType t => t -> Type
getType forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (forall a. a -> [a] -> [a]
: [])) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t
  typecheckTuple Mode
mode (Term
t : [Term]
ts) = do
    (Mode
m, Mode
ms) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
CProd Mode
mode (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Term] -> Term
TTup (Term
t forall a. a -> [a] -> [a]
: [Term]
ts))
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
m Term
t
    (Type
ty, [ATerm]
ats) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
ms [Term]
ts
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. HasType t => t -> Type
getType ATerm
at Type -> Type -> Type
:*: Type
ty, ATerm
at forall a. a -> [a] -> [a]
: [ATerm]
ats)

----------------------------------------
-- Comparison chain

typecheck Mode
Infer (TChain Term
t [Link_ UD]
ls) =
  Type -> ATerm -> [Link_ TY] -> ATerm
ATChain Type
TyBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
t [Link_ UD]
ls
 where
  inferChain ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Term ->
    [Link] ->
    Sem r [ALink]
  inferChain :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
  inferChain Term
t1 (TLink BOp
op Term
t2 : [Link_ UD]
links) = do
    ATerm
at2 <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t2
    ATerm
_ <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check (BOp -> Term -> Term -> Term
TBin BOp
op Term
t1 Term
t2) Type
TyBool
    [Link_ TY]
atl <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
t2 [Link_ UD]
links
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ BOp -> ATerm -> Link_ TY
ATLink BOp
op ATerm
at2 forall a. a -> [a] -> [a]
: [Link_ TY]
atl

----------------------------------------
-- Type operations

typecheck Mode
Infer (TTyOp TyOp
Enumerate Type
t) = do
  forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> TyOp -> Type -> ATerm
ATTyOp (Type -> Type
TyList Type
t) TyOp
Enumerate Type
t
typecheck Mode
Infer (TTyOp TyOp
Count Type
t) = do
  forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> TyOp -> Type -> ATerm
ATTyOp (Type
TyUnit Type -> Type -> Type
:+: Type
TyN) TyOp
Count Type
t

--------------------------------------------------
-- Containers

-- Literal containers, including ellipses
typecheck Mode
mode t :: Term
t@(TContainer Container
c [(Term, Maybe Term)]
xs Maybe (Ellipsis Term)
ell) = do
  Mode
eltMode <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 (Container -> Con
containerToCon Container
c) Mode
mode (forall a b. a -> Either a b
Left Term
t)
  [(ATerm, Maybe ATerm)]
axns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Term
x, Maybe Term
n) -> (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
eltMode Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
`check` Type
TyN) Maybe Term
n) [(Term, Maybe Term)]
xs
  Maybe (Ellipsis ATerm)
aell <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
typecheckEllipsis Mode
eltMode Maybe (Ellipsis Term)
ell
  Type
resTy <- case Mode
mode of
    Mode
Infer -> do
      let tys :: [Type]
tys = [forall t. HasType t => t -> Type
getType ATerm
at | Just (Until ATerm
at) <- [Maybe (Ellipsis ATerm)
aell]] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall t. HasType t => t -> Type
getType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ATerm, Maybe ATerm)]
axns
      Type
tyv <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      forall (r :: EffectRow).
Member (Writer Constraint) r =>
[Constraint] -> Sem r ()
constraints forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type -> Constraint
`CSub` Type
tyv) [Type]
tys
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Container -> Type -> Type
containerTy Container
c Type
tyv
    Check Type
ty -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
  Type
eltTy <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Container -> Type -> Sem r Type
getEltTy Container
c Type
resTy

  -- See Note [Container literal constraints]
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Container
c forall a. Eq a => a -> a -> Bool
/= Container
ListContainer Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(Term, Maybe Term)]
xs)) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
eltTy
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isJust Maybe (Ellipsis Term)
ell) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QEnum Type
eltTy
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer Type
resTy Container
c [(ATerm, Maybe ATerm)]
axns Maybe (Ellipsis ATerm)
aell
 where
  typecheckEllipsis ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Mode ->
    Maybe (Ellipsis Term) ->
    Sem r (Maybe (Ellipsis ATerm))
  typecheckEllipsis :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
typecheckEllipsis Mode
_ Maybe (Ellipsis Term)
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  typecheckEllipsis Mode
m (Just (Until Term
tm)) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. t -> Ellipsis t
Until forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
m Term
tm

-- ~~~~ Note [Container literal constraints]
--
-- It should only be possible to construct something of type Set(a) or
-- Bag(a) when a is comparable, so we can normalize the set or bag
-- value.  For example, Set(N) is OK, but Set(N -> N) is not.  On the
-- other hand, List(a) is fine for any type a.  We want to maintain
-- the invariant that we can only actually obtain a value of type
-- Set(a) or Bag(a) if a is comparable.  This means we will be able to
-- write polymorphic functions that take bags or sets as input without
-- having to specify any constraints --- the only way to call such
-- functions is with element types that actually support comparison.
-- For example, 'unions' can simply have the type Set(Set(a)) ->
-- Set(a).
--
-- Hence, container literals (along with the 'set' and 'bag'
-- conversion functions) serve as "gatekeepers" to make sure we can
-- only construct containers with appropriate element types.  So when
-- we see a container literal, if it is a bag or set literal, we have
-- to introduce an additional QCmp constraint for the element type.
--
-- But not so fast --- with that rule, 'unions' does not type check!
-- To see why, look at the definition:
--
--   unions(ss) = foldr(~∪~, {}, list(ss))
--
-- The empty set literal in the definition means we end up generating
-- a QCmp constraint on the element type anyway.  But there is a
-- solution: we refine our invariant to say that we can only
-- actually obtain a *non-empty* value of type Set(a) or Bag(a) if a
-- is comparable.  Empty bags and sets are allowed to have any element
-- type.  This is safe because there is no way to generate a non-empty
-- set from an empty one, without also making use of something like a
-- non-empty set literal or conversion function.  So we add a special
-- case to the rule that says we only add a QCmp constraint in the
-- case of a *non-empty* set or bag literal.  Now the definition of
-- 'unions' type checks perfectly well.

-- Container comprehensions
typecheck Mode
mode tcc :: Term
tcc@(TContainerComp Container
c Bind (Telescope (Qual_ UD)) Term
bqt) = do
  Mode
eltMode <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 (Container -> Con
containerToCon Container
c) Mode
mode (forall a b. a -> Either a b
Left Term
tcc)
  (Telescope (Qual_ UD)
qs, Term
t) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Qual_ UD)) Term
bqt
  (Telescope (Qual_ TY)
aqs, TyCtx
cx) <- forall b tyb (r :: EffectRow).
(Alpha b, Alpha tyb, Member (Reader TyCtx) r) =>
(b -> Sem r (tyb, TyCtx))
-> Telescope b -> Sem r (Telescope tyb, TyCtx)
inferTelescope forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Qual_ UD -> Sem r (Qual_ TY, TyCtx)
inferQual Telescope (Qual_ UD)
qs
  forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
cx forall a b. (a -> b) -> a -> b
$ do
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
eltMode Term
t
    let resTy :: Type
resTy = case Mode
mode of
          Mode
Infer -> Container -> Type -> Type
containerTy Container
c (forall t. HasType t => t -> Type
getType ATerm
at)
          Check Type
ty -> Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Container -> Bind (Telescope (Qual_ TY)) ATerm -> ATerm
ATContainerComp Type
resTy Container
c (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Qual_ TY)
aqs ATerm
at)
 where
  inferQual ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Qual ->
    Sem r (AQual, TyCtx)
  inferQual :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Qual_ UD -> Sem r (Qual_ TY, TyCtx)
inferQual (QBind Name Term
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
t
    Type
ty <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 (Container -> Con
containerToCon Container
c) (forall t. HasType t => t -> Type
getType ATerm
at) (forall a b. a -> Either a b
Left Embedded (Embed Term)
t)
    forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Embed ATerm -> Qual_ TY
AQBind (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x) (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at), forall a b. QName a -> b -> Ctx a b
singleCtx (forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType Type
ty))
  inferQual (QGuard (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
t Type
TyBool
    forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> Qual_ TY
AQGuard (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at), forall a b. Ctx a b
emptyCtx)

--------------------------------------------------
-- Let

-- To check/infer a let expression.  Note let is non-recursive.
typecheck Mode
mode (TLet Bind (Telescope (Binding_ UD)) Term
l) = do
  (Telescope (Binding_ UD)
bs, Term
t2) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Binding_ UD)) Term
l

  -- Infer the types of all the variables bound by the let...
  (Telescope (Binding_ TY)
as, TyCtx
ctx) <- forall b tyb (r :: EffectRow).
(Alpha b, Alpha tyb, Member (Reader TyCtx) r) =>
(b -> Sem r (tyb, TyCtx))
-> Telescope b -> Sem r (Telescope tyb, TyCtx)
inferTelescope forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Binding_ UD -> Sem r (Binding_ TY, TyCtx)
inferBinding Telescope (Binding_ UD)
bs

  -- ...then check/infer the body under an extended context.
  forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx forall a b. (a -> b) -> a -> b
$ do
    ATerm
at2 <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> Bind (Telescope (Binding_ TY)) ATerm -> ATerm
ATLet (forall t. HasType t => t -> Type
getType ATerm
at2) (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Binding_ TY)
as ATerm
at2)
 where
  -- Infer the type of a binding (@x [: ty] = t@), returning a
  -- type-annotated binding along with a (singleton) context for the
  -- bound variable.  The optional type annotation on the variable
  -- determines whether we use inference or checking mode for the
  -- body.
  inferBinding ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Binding ->
    Sem r (ABinding, TyCtx)
  inferBinding :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Binding_ UD -> Sem r (Binding_ TY, TyCtx)
inferBinding (Binding Maybe (Embed PolyType)
mty Name Term
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
    ATerm
at <- case Maybe (Embed PolyType)
mty of
      Just (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty) -> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Embedded (Embed Term)
t Embedded (Embed PolyType)
ty
      Maybe (Embed PolyType)
Nothing -> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
t
    forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> Binding_ TY
ABinding Maybe (Embed PolyType)
mty (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x) (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at), forall a b. QName a -> b -> Ctx a b
singleCtx (forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType forall a b. (a -> b) -> a -> b
$ forall t. HasType t => t -> Type
getType ATerm
at))

--------------------------------------------------
-- Case

-- Check/infer a case expression.
typecheck Mode
_ (TCase []) = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw TCError
EmptyCase
typecheck Mode
mode (TCase [Branch]
bs) = do
  [ABranch]
bs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Branch -> Sem r ABranch
typecheckBranch [Branch]
bs
  Type
resTy <- case Mode
mode of
    Check Type
ty -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    Mode
Infer -> do
      Type
x <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      forall (r :: EffectRow).
Member (Writer Constraint) r =>
[Constraint] -> Sem r ()
constraints forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type -> Constraint
`CSub` Type
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasType t => t -> Type
getType) [ABranch]
bs'
      forall (m :: * -> *) a. Monad m => a -> m a
return Type
x
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> [ABranch] -> ATerm
ATCase Type
resTy [ABranch]
bs'
 where
  typecheckBranch ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Branch ->
    Sem r ABranch
  typecheckBranch :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Branch -> Sem r ABranch
typecheckBranch Branch
b = do
    (Telescope (Guard_ UD)
gs, Term
t) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Branch
b
    (Telescope (Guard_ TY)
ags, TyCtx
ctx) <- forall b tyb (r :: EffectRow).
(Alpha b, Alpha tyb, Member (Reader TyCtx) r) =>
(b -> Sem r (tyb, TyCtx))
-> Telescope b -> Sem r (Telescope tyb, TyCtx)
inferTelescope forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Guard_ UD -> Sem r (Guard_ TY, TyCtx)
inferGuard Telescope (Guard_ UD)
gs
    forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx forall a b. (a -> b) -> a -> b
$
      forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Guard_ TY)
ags forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t

  -- Infer the type of a guard, returning the type-annotated guard
  -- along with a context of types for any variables bound by the
  -- guard.
  inferGuard ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Guard ->
    Sem r (AGuard, TyCtx)
  inferGuard :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Guard_ UD -> Sem r (Guard_ TY, TyCtx)
inferGuard (GBool (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
t Type
TyBool
    forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> Guard_ TY
AGBool (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at), forall a b. Ctx a b
emptyCtx)
  inferGuard (GPat (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) Pattern
p) = do
    ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
t
    (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p (forall t. HasType t => t -> Type
getType ATerm
at)
    forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> APattern -> Guard_ TY
AGPat (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at) APattern
apt, TyCtx
ctx)
  inferGuard (GLet (Binding Maybe (Embed PolyType)
mty Name Term
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t))) = do
    ATerm
at <- case Maybe (Embed PolyType)
mty of
      Just (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty) -> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Embedded (Embed Term)
t Embedded (Embed PolyType)
ty
      Maybe (Embed PolyType)
Nothing -> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
t
    forall (m :: * -> *) a. Monad m => a -> m a
return
      ( Binding_ TY -> Guard_ TY
AGLet (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> Binding_ TY
ABinding Maybe (Embed PolyType)
mty (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x) (forall e. IsEmbed e => Embedded e -> e
embed ATerm
at))
      , forall a b. QName a -> b -> Ctx a b
singleCtx (forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType (forall t. HasType t => t -> Type
getType ATerm
at))
      )

--------------------------------------------------
-- Type ascription

-- Ascriptions are what let us flip from inference mode into
-- checking mode.
typecheck Mode
Infer (TAscr Term
t PolyType
ty) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid PolyType
ty forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t PolyType
ty
--------------------------------------------------
-- Inference fallback

-- Finally, to check anything else, we can fall back to inferring its
-- type and then check that the inferred type is a *subtype* of the
-- given type.  We have to be careful to call 'setType' to change the
-- type at the root of the term to the requested type.
typecheck (Check Type
ty) Term
t = do
  ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub (forall t. HasType t => t -> Type
getType ATerm
at) Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. HasType t => Type -> t -> t
setType Type
ty ATerm
at

------------------------------------------------------------
-- Patterns
------------------------------------------------------------

-- | Check that a pattern has the given type, and return a context of
--   pattern variables bound in the pattern along with their types.
checkPattern ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Pattern ->
  Type ->
  Sem r (TyCtx, APattern)
checkPattern :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern (PNonlinear Pattern
p Name Term
x) Type
_ = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ Pattern -> Name Term -> TCError
NonlinearPattern Pattern
p Name Term
x
checkPattern Pattern
p (TyUser String
name [Type]
args) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p
checkPattern (PVar Name Term
x) Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. QName a -> b -> Ctx a b
singleCtx (forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType Type
ty), Type -> Name ATerm -> APattern
APVar Type
ty (coerce :: forall a b. Coercible a b => a -> b
coerce Name Term
x))
checkPattern Pattern
PWild Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, Type -> APattern
APWild Type
ty)
checkPattern (PAscr Pattern
p Type
ty1) Type
ty2 = do
  -- We have a pattern that promises to match ty1 and someone is asking
  -- us if it can also match ty2. So we just have to ensure what we're
  -- being asked for is a subtype of what we can promise to cover...
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
ty2 Type
ty1
  -- ... and then make sure the pattern can actually match what it promised to.
  forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1
checkPattern Pattern
PUnit Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyUnit
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, APattern
APUnit)
checkPattern (PBool Bool
b) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyBool
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, Bool -> APattern
APBool Bool
b)
checkPattern (PChar Char
c) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyC
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, Char -> APattern
APChar Char
c)
checkPattern (PString String
s) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyString
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, String -> APattern
APString String
s)
checkPattern (PTup [Pattern]
tup) Type
tupTy = do
  [(TyCtx, APattern)]
listCtxtAps <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [Pattern]
tup Type
tupTy
  let ([TyCtx]
ctxs, [APattern]
aps) = forall a b. [(a, b)] -> ([a], [b])
unzip [(TyCtx, APattern)]
listCtxtAps
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Monoid a => [a] -> a
mconcat [TyCtx]
ctxs, Type -> [APattern] -> APattern
APTup (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
(:*:) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasType t => t -> Type
getType [APattern]
aps)) [APattern]
aps)
 where
  checkTuplePat ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    [Pattern] ->
    Type ->
    Sem r [(TyCtx, APattern)]
  checkTuplePat :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [] Type
_ = forall a. HasCallStack => String -> a
error String
"Impossible! checkTuplePat []"
  checkTuplePat [Pattern
p] Type
ty = do
    -- (:[]) <$> check t ty
    (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
    forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCtx
ctx, APattern
apt)]
  checkTuplePat (Pattern
p : [Pattern]
ps) Type
ty = do
    (Type
ty1, Type
ty2) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CProd Type
ty (forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [Pattern] -> Pattern
PTup (Pattern
p forall a. a -> [a] -> [a]
: [Pattern]
ps))
    (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1
    [(TyCtx, APattern)]
rest <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [Pattern]
ps Type
ty2
    forall (m :: * -> *) a. Monad m => a -> m a
return ((TyCtx
ctx, APattern
apt) forall a. a -> [a] -> [a]
: [(TyCtx, APattern)]
rest)
checkPattern p :: Pattern
p@(PInj Side
L Pattern
pat) Type
ty = do
  (Type
ty1, Type
ty2) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CSum Type
ty (forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty1
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> Side -> APattern -> APattern
APInj (Type
ty1 Type -> Type -> Type
:+: Type
ty2) Side
L APattern
apt)
checkPattern p :: Pattern
p@(PInj Side
R Pattern
pat) Type
ty = do
  (Type
ty1, Type
ty2) <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CSum Type
ty (forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty2
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> Side -> APattern -> APattern
APInj (Type
ty1 Type -> Type -> Type
:+: Type
ty2) Side
R APattern
apt)

-- we can match any supertype of TyN against a Nat pattern, OR
-- any TyFin.

-- XXX this isn't quite right, what if we're checking at a type
-- variable but we need to solve it to be a TyFin?  Can this ever
-- happen?  We would need a COr, except we can't express the
-- constraint "exists m. ty = TyFin m"
--
-- Yes, this can happen, and here's an example:
--
--   > (\x. {? true when x is 3, false otherwise ?}) (2 : Z5)
--   Unsolvable NoUnify
--   > (\(x : Z5). {? true when x is 3, false otherwise ?}) (2 : Z5)
--   false

-- checkPattern (PNat n) (TyFin m) = return (emptyCtx, APNat (TyFin m) n)
checkPattern (PNat Integer
n) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
TyN Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ctx a b
emptyCtx, Type -> Integer -> APattern
APNat Type
ty Integer
n)
checkPattern p :: Pattern
p@(PCons Pattern
p1 Pattern
p2) Type
ty = do
  Type
tyl <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
CList Type
ty (forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx1, APattern
ap1) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p1 Type
tyl
  (TyCtx
ctx2, APattern
ap2) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p2 (Type -> Type
TyList Type
tyl)
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx1 forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx2, Type -> APattern -> APattern -> APattern
APCons (Type -> Type
TyList Type
tyl) APattern
ap1 APattern
ap2)
checkPattern p :: Pattern
p@(PList [Pattern]
ps) Type
ty = do
  Type
tyl <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
CList Type
ty (forall a b. b -> Either a b
Right Pattern
p)
  [(TyCtx, APattern)]
listCtxtAps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
`checkPattern` Type
tyl) [Pattern]
ps
  let ([TyCtx]
ctxs, [APattern]
aps) = forall a b. [(a, b)] -> ([a], [b])
unzip [(TyCtx, APattern)]
listCtxtAps
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Monoid a => [a] -> a
mconcat [TyCtx]
ctxs, Type -> [APattern] -> APattern
APList (Type -> Type
TyList Type
tyl) [APattern]
aps)
checkPattern (PAdd Side
s Pattern
p Term
t) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> Side -> APattern -> ATerm -> APattern
APAdd Type
ty Side
s APattern
apt ATerm
at)
checkPattern (PMul Side
s Pattern
p Term
t) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> Side -> APattern -> ATerm -> APattern
APMul Type
ty Side
s APattern
apt ATerm
at)
checkPattern (PSub Pattern
p Term
t) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> APattern -> ATerm -> APattern
APSub Type
ty APattern
apt ATerm
at)
checkPattern (PNeg Pattern
p) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSub Type
ty
  Type
tyInner <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
ty
  (TyCtx
ctx, APattern
apt) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
tyInner
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx, Type -> APattern -> APattern
APNeg Type
ty APattern
apt)
checkPattern (PFrac Pattern
p Pattern
q) Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QDiv Type
ty
  Type
tyP <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
ty
  Type
tyQ <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
tyP
  (TyCtx
ctx1, APattern
ap1) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
tyP
  (TyCtx
ctx2, APattern
ap2) <- forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
q Type
tyQ
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx1 forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx2, Type -> APattern -> APattern -> APattern
APFrac Type
ty APattern
ap1 APattern
ap2)

------------------------------------------------------------
-- Constraints for abs, floor/ceiling/idiv, and exp
------------------------------------------------------------

-- | Constraints needed on a function type for it to be the type of
--   the absolute value function.
cAbs :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r ()
cAbs :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r ()
cAbs Type
argTy Type
resTy = do
  Type
resTy' <- forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
argTy
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
resTy Type
resTy'

-- | Constraints needed on a function type for it to be the type of
--   the container size operation.
cSize :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r ()
cSize :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r ()
cSize Type
argTy Type
resTy = do
  Type
a <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  Atom
c <- forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Atom -> Type -> Type
TyContainer Atom
c Type
a) Type
argTy
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
TyN Type
resTy

-- | Given an input type @ty@, return a type which represents the
--   output type of the absolute value function, and generate
--   appropriate constraints.
cPos :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type
cPos :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty -- The input type has to be numeric.
  case Type
ty of
    -- If the input type is a concrete base type, we can just
    -- compute the correct output type.
    TyAtom (ABase BaseTy
b) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type
TyAtom (BaseTy -> Atom
ABase (BaseTy -> BaseTy
pos BaseTy
b))
    -- Otherwise, generate a fresh type variable for the output type
    -- along with some constraints.
    Type
_ -> do
      Type
res <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy

      -- Valid types for absolute value are Z -> N, Q -> F, or T -> T
      -- (e.g. Z5 -> Z5).
      forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
        [Constraint] -> Constraint
COr
          [ [Constraint] -> Constraint
cAnd [Type -> Type -> Constraint
CSub Type
ty Type
TyZ, Type -> Type -> Constraint
CSub Type
TyN Type
res]
          , [Constraint] -> Constraint
cAnd [Type -> Type -> Constraint
CSub Type
ty Type
TyQ, Type -> Type -> Constraint
CSub Type
TyF Type
res]
          , Type -> Type -> Constraint
CEq Type
ty Type
res
          ]
      forall (m :: * -> *) a. Monad m => a -> m a
return Type
res
 where
  pos :: BaseTy -> BaseTy
pos BaseTy
Z = BaseTy
N
  pos BaseTy
Q = BaseTy
F
  pos BaseTy
t = BaseTy
t

-- | Given an input type @ty@, return a type which represents the
--   output type of the floor or ceiling functions, and generate
--   appropriate constraints.
cInt :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type
cInt :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
ty = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  case Type
ty of
    -- If the input type is a concrete base type, we can just
    -- compute the correct output type.
    TyAtom (ABase BaseTy
b) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom -> Type
TyAtom (BaseTy -> Atom
ABase (BaseTy -> BaseTy
int BaseTy
b))
    -- Otherwise, generate a fresh type variable for the output type
    -- along with some constraints.
    Type
_ -> do
      Type
res <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy

      -- Valid types for absolute value are F -> N, Q -> Z, or T -> T
      -- (e.g. Z5 -> Z5).
      forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
        [Constraint] -> Constraint
COr
          [ [Constraint] -> Constraint
cAnd [Type -> Type -> Constraint
CSub Type
ty Type
TyF, Type -> Type -> Constraint
CSub Type
TyN Type
res]
          , [Constraint] -> Constraint
cAnd [Type -> Type -> Constraint
CSub Type
ty Type
TyQ, Type -> Type -> Constraint
CSub Type
TyZ Type
res]
          , Type -> Type -> Constraint
CEq Type
ty Type
res
          ]
      forall (m :: * -> *) a. Monad m => a -> m a
return Type
res
 where
  int :: BaseTy -> BaseTy
int BaseTy
F = BaseTy
N
  int BaseTy
Q = BaseTy
Z
  int BaseTy
t = BaseTy
t

-- | Given input types to the exponentiation operator, return a type
--   which represents the output type, and generate appropriate
--   constraints.
cExp :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r Type
cExp :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r Type
cExp Type
ty1 Type
TyN = do
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty1
  forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty1

-- We could include a special case for TyZ, but for that we would need
-- a function to find a supertype of a given type that satisfies QDiv.

cExp Type
ty1 Type
ty2 = do
  -- Create a fresh type variable to represent the result type.  The
  -- base type has to be a subtype.
  Type
resTy <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
ty1 Type
resTy

  -- Either the exponent type is N, in which case the result type has
  -- to support multiplication, or else the exponent is Z, in which
  -- case the result type also has to support division.
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$
    [Constraint] -> Constraint
COr
      [ [Constraint] -> Constraint
cAnd [Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
resTy, Type -> Type -> Constraint
CEq Type
ty2 Type
TyN]
      , [Constraint] -> Constraint
cAnd [Qualifier -> Type -> Constraint
CQual Qualifier
QDiv Type
resTy, Type -> Type -> Constraint
CEq Type
ty2 Type
TyZ]
      ]
  forall (m :: * -> *) a. Monad m => a -> m a
return Type
resTy

------------------------------------------------------------
-- Decomposing type constructors
------------------------------------------------------------

-- | Get the argument (element) type of a (known) container type.  Returns a
--   fresh variable with a suitable constraint if the given type is
--   not literally a container type.
getEltTy :: Members '[Writer Constraint, Fresh] r => Container -> Type -> Sem r Type
getEltTy :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Container -> Type -> Sem r Type
getEltTy Container
_ (TyContainer Atom
_ Type
e) = forall (m :: * -> *) a. Monad m => a -> m a
return Type
e
getEltTy Container
c Type
ty = do
  Type
eltTy <- forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Container -> Type -> Type
containerTy Container
c Type
eltTy) Type
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return Type
eltTy

-- | Ensure that a type's outermost constructor matches the provided
--   constructor, returning the types within the matched constructor
--   or throwing a type error.  If the type provided is a type
--   variable, appropriate constraints are generated to guarantee the
--   type variable's outermost constructor matches the provided
--   constructor, and a list of fresh type variables is returned whose
--   count matches the arity of the provided constructor.
ensureConstr ::
  forall r.
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Type ->
  Either Term Pattern ->
  Sem r [Type]
ensureConstr :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
targ = Con -> Type -> Sem r [Type]
matchConTy Con
c Type
ty
 where
  matchConTy :: Con -> Type -> Sem r [Type]

  -- expand type definitions lazily
  matchConTy :: Con -> Type -> Sem r [Type]
matchConTy Con
c1 (TyUser String
name [Type]
args) = forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Con -> Type -> Sem r [Type]
matchConTy Con
c1
  matchConTy Con
c1 (TyCon Con
c2 [Type]
tys) = do
    Con -> Con -> Sem r ()
matchCon Con
c1 Con
c2
    forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tys
  matchConTy Con
c1 tyv :: Type
tyv@(TyAtom (AVar (U Name Type
_))) = do
    [Type]
tyvs <- 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 forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy) (Con -> [Variance]
arity Con
c1)
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
tyv (Con -> [Type] -> Type
TyCon Con
c1 [Type]
tyvs)
    forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tyvs
  matchConTy Con
_ Type
_ = forall a. Sem r a
matchError

  -- \| Check whether two constructors match, which could include
  --   unifying container variables if we are matching two container
  --   types; otherwise, simply ensure that the constructors are
  --   equal.  Throw a 'matchError' if they do not match.
  matchCon :: Con -> Con -> Sem r ()
  matchCon :: Con -> Con -> Sem r ()
matchCon Con
c1 Con
c2 | Con
c1 forall a. Eq a => a -> a -> Bool
== Con
c2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  matchCon (CContainer v :: Atom
v@(AVar (U Name Type
_))) (CContainer Atom
ctr2) =
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom Atom
v) (Atom -> Type
TyAtom Atom
ctr2)
  matchCon (CContainer Atom
ctr1) (CContainer v :: Atom
v@(AVar (U Name Type
_))) =
    forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom Atom
ctr1) (Atom -> Type
TyAtom Atom
v)
  matchCon Con
_ Con
_ = forall a. Sem r a
matchError

  matchError :: Sem r a
  matchError :: forall a. Sem r a
matchError = case Either Term Pattern
targ of
    Left Term
term -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> Term -> Type -> TCError
NotCon Con
c Term
term Type
ty)
    Right Pattern
pat -> forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> Pattern -> Type -> TCError
PatternType Con
c Pattern
pat Type
ty)

-- | A variant of ensureConstr that expects to get exactly one
--   argument type out, and throws an error if we get any other
--   number.
ensureConstr1 ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Type ->
  Either Term Pattern ->
  Sem r Type
ensureConstr1 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
c Type
ty Either Term Pattern
targ = do
  [Type]
tys <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
targ
  case [Type]
tys of
    [Type
ty1] -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty1
    [Type]
_ ->
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Impossible! Wrong number of arg types in ensureConstr1 "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c
          forall a. [a] -> [a] -> [a]
++ String
" "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty
          forall a. [a] -> [a] -> [a]
++ String
": "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Type]
tys

-- | A variant of ensureConstr that expects to get exactly two
--   argument types out, and throws an error if we get any other
--   number.
ensureConstr2 ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Type ->
  Either Term Pattern ->
  Sem r (Type, Type)
ensureConstr2 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
c Type
ty Either Term Pattern
targ = do
  [Type]
tys <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
targ
  case [Type]
tys of
    [Type
ty1, Type
ty2] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty1, Type
ty2)
    [Type]
_ ->
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Impossible! Wrong number of arg types in ensureConstr2 "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c
          forall a. [a] -> [a] -> [a]
++ String
" "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty
          forall a. [a] -> [a] -> [a]
++ String
": "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Type]
tys

-- | A variant of 'ensureConstr' that works on 'Mode's instead of
--   'Type's.  Behaves similarly to 'ensureConstr' if the 'Mode' is
--   'Check'; otherwise it generates an appropriate number of copies
--   of 'Infer'.
ensureConstrMode ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Mode ->
  Either Term Pattern ->
  Sem r [Mode]
ensureConstrMode :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
Infer Either Term Pattern
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> b -> a
const Mode
Infer) (Con -> [Variance]
arity Con
c)
ensureConstrMode Con
c (Check Type
ty) Either Term Pattern
tp = forall a b. (a -> b) -> [a] -> [b]
map Type -> Mode
Check forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
tp

-- | A variant of 'ensureConstrMode' that expects to get a single
--   'Mode' and throws an error if it encounters any other number.
ensureConstrMode1 ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Mode ->
  Either Term Pattern ->
  Sem r Mode
ensureConstrMode1 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
m Either Term Pattern
targ
  case [Mode]
ms of
    [Mode
m1] -> forall (m :: * -> *) a. Monad m => a -> m a
return Mode
m1
    [Mode]
_ ->
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Impossible! Wrong number of arg types in ensureConstrMode1 "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c
          forall a. [a] -> [a] -> [a]
++ String
" "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Mode
m
          forall a. [a] -> [a] -> [a]
++ String
": "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Mode]
ms

-- | A variant of 'ensureConstrMode' that expects to get two 'Mode's
--   and throws an error if it encounters any other number.
ensureConstrMode2 ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Mode ->
  Either Term Pattern ->
  Sem r (Mode, Mode)
ensureConstrMode2 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
m Either Term Pattern
targ
  case [Mode]
ms of
    [Mode
m1, Mode
m2] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Mode
m1, Mode
m2)
    [Mode]
_ ->
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Impossible! Wrong number of arg types in ensureConstrMode2 "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c
          forall a. [a] -> [a] -> [a]
++ String
" "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Mode
m
          forall a. [a] -> [a] -> [a]
++ String
": "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Mode]
ms

-- | Ensure that two types are equal:
--     1. Do nothing if they are literally equal
--     2. Generate an equality constraint otherwise
ensureEq :: Member (Writer Constraint) r => Type -> Type -> Sem r ()
ensureEq :: forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty1 Type
ty2
  | Type
ty1 forall a. Eq a => a -> a -> Bool
== Type
ty2 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
ty1 Type
ty2