{-# 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 :: (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 (Telescope b -> [b]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope b
tel)
  (Telescope tyb, TyCtx) -> Sem r (Telescope tyb, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return ([tyb] -> Telescope tyb
forall b. Alpha b => [b] -> Telescope b
toTelescope [tyb]
tel1, TyCtx
ctx)
  where
    go :: [b] -> Sem r ([tyb], TyCtx)
go []     = ([tyb], TyCtx) -> Sem r ([tyb], TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], TyCtx
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
      TyCtx -> Sem r ([tyb], TyCtx) -> Sem r ([tyb], TyCtx)
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx (Sem r ([tyb], TyCtx) -> Sem r ([tyb], TyCtx))
-> Sem r ([tyb], TyCtx) -> Sem r ([tyb], TyCtx)
forall a b. (a -> b) -> a -> b
$ do
      ([tyb]
tybs, TyCtx
ctx') <- [b] -> Sem r ([tyb], TyCtx)
go [b]
bs
      ([tyb], TyCtx) -> Sem r ([tyb], TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (tyb
tybtyb -> [tyb] -> [tyb]
forall a. a -> [a] -> [a]
:[tyb]
tybs, TyCtx
ctx TyCtx -> TyCtx -> TyCtx
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, Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r
  => ModuleName -> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo
checkModule :: 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 = [TyCtx] -> TyCtx
forall a. Monoid a => [a] -> a
mconcat (Map ModuleName ModuleInfo
imports Map ModuleName ModuleInfo
-> Getting (Endo [TyCtx]) (Map ModuleName ModuleInfo) TyCtx
-> [TyCtx]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo))
-> ((TyCtx -> Const (Endo [TyCtx]) TyCtx)
    -> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> Getting (Endo [TyCtx]) (Map ModuleName ModuleInfo) TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Const (Endo [TyCtx]) TyCtx)
-> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo
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 :: Map String TyDefBody
importTyDefnCtx = [Map String TyDefBody] -> Map String TyDefBody
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions (Map ModuleName ModuleInfo
imports Map ModuleName ModuleInfo
-> Getting
     (Endo [Map String TyDefBody])
     (Map ModuleName ModuleInfo)
     (Map String TyDefBody)
-> [Map String TyDefBody]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (ModuleInfo -> Const (Endo [Map String TyDefBody]) ModuleInfo)
-> Map ModuleName ModuleInfo
-> Const (Endo [Map String TyDefBody]) (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ModuleInfo -> Const (Endo [Map String TyDefBody]) ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const (Endo [Map String TyDefBody]) (Map ModuleName ModuleInfo))
-> ((Map String TyDefBody
     -> Const (Endo [Map String TyDefBody]) (Map String TyDefBody))
    -> ModuleInfo -> Const (Endo [Map String TyDefBody]) ModuleInfo)
-> Getting
     (Endo [Map String TyDefBody])
     (Map ModuleName ModuleInfo)
     (Map String TyDefBody)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map String TyDefBody
 -> Const (Endo [Map String TyDefBody]) (Map String TyDefBody))
-> ModuleInfo -> Const (Endo [Map String TyDefBody]) ModuleInfo
Lens' ModuleInfo (Map String TyDefBody)
miTydefs)
  Map String TyDefBody
tyDefnCtx <- (TCError -> LocTCError)
-> Sem (Error TCError : r) (Map String TyDefBody)
-> Sem r (Map String TyDefBody)
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc (Sem (Error TCError : r) (Map String TyDefBody)
 -> Sem r (Map String TyDefBody))
-> Sem (Error TCError : r) (Map String TyDefBody)
-> Sem r (Map String TyDefBody)
forall a b. (a -> b) -> a -> b
$ [TypeDefn] -> Sem (Error TCError : r) (Map String TyDefBody)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
[TypeDefn] -> Sem r (Map String TyDefBody)
makeTyDefnCtx [TypeDefn]
tydefs
  Map String TyDefBody -> Sem r ModuleInfo -> Sem r ModuleInfo
forall (r :: EffectRow) a.
Member (Reader (Map String TyDefBody)) r =>
Map String TyDefBody -> Sem r a -> Sem r a
withTyDefns (Map String TyDefBody
tyDefnCtx Map String TyDefBody
-> Map String TyDefBody -> Map String TyDefBody
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map String TyDefBody
importTyDefnCtx) (Sem r ModuleInfo -> Sem r ModuleInfo)
-> Sem r ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
    TyCtx
tyCtx     <- (TCError -> LocTCError)
-> Sem (Error TCError : r) TyCtx -> Sem r 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 (Sem (Error TCError : r) TyCtx -> Sem r TyCtx)
-> Sem (Error TCError : r) TyCtx -> Sem r TyCtx
forall a b. (a -> b) -> a -> b
$ ModuleName -> [TypeDecl] -> Sem (Error TCError : r) TyCtx
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx ModuleName
name [TypeDecl]
typeDecls
    TyCtx -> Sem r ModuleInfo -> Sem r ModuleInfo
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
importTyCtx (Sem r ModuleInfo -> Sem r ModuleInfo)
-> Sem r ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ TyCtx -> Sem r ModuleInfo -> Sem r ModuleInfo
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
tyCtx (Sem r ModuleInfo -> Sem r ModuleInfo)
-> Sem r ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ do
      (TypeDefn -> Sem r ()) -> [TypeDefn] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ModuleName -> TypeDefn -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error LocTCError] r =>
ModuleName -> TypeDefn -> Sem r ()
checkTyDefn ModuleName
name) [TypeDefn]
tydefs
      [Defn]
adefns <- (TermDefn -> Sem r Defn) -> [TermDefn] -> Sem r [Defn]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ModuleName -> TermDefn -> Sem r Defn
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Error LocTCError,
    Fresh, Output Message]
  r =>
ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name) [TermDefn]
defns
      let defnCtx :: Ctx ATerm Defn
defnCtx = ModuleName -> [(Name ATerm, Defn)] -> Ctx ATerm Defn
forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name ((Defn -> (Name ATerm, Defn)) -> [Defn] -> [(Name ATerm, Defn)]
forall a b. (a -> b) -> [a] -> [b]
map (Defn -> Name ATerm
getDefnName (Defn -> Name ATerm)
-> (Defn -> Defn) -> Defn -> (Name ATerm, Defn)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Defn -> Defn
forall a. a -> a
id) [Defn]
adefns)
          docCtx :: Ctx Term Docs
docCtx = ModuleName -> [(Name Term, Docs)] -> Ctx Term Docs
forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name [(Name Term, Docs)]
docs
          dups :: [Name ATerm]
dups = [Name ATerm] -> [Name ATerm]
forall a. Ord a => [a] -> [a]
filterDups ([Name ATerm] -> [Name ATerm])
-> ([Defn] -> [Name ATerm]) -> [Defn] -> [Name ATerm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Name ATerm) -> [Defn] -> [Name ATerm]
forall a b. (a -> b) -> [a] -> [b]
map Defn -> Name ATerm
getDefnName ([Defn] -> [Name ATerm]) -> [Defn] -> [Name ATerm]
forall a b. (a -> b) -> a -> b
$ [Defn]
adefns
      case [Name ATerm]
dups of
        (Name ATerm
x:[Name ATerm]
_) -> LocTCError -> Sem r ModuleInfo
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (LocTCError -> Sem r ModuleInfo) -> LocTCError -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCError -> LocTCError
noLoc (TCError -> LocTCError) -> TCError -> LocTCError
forall a b. (a -> b) -> a -> b
$ Name Term -> TCError
DuplicateDefns (Name ATerm -> Name Term
coerce Name ATerm
x)
        [] -> do
          Ctx ATerm [ATerm]
aprops <- (TCError -> LocTCError)
-> Sem (Error TCError : r) (Ctx ATerm [ATerm])
-> Sem r (Ctx ATerm [ATerm])
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc (Sem (Error TCError : r) (Ctx ATerm [ATerm])
 -> Sem r (Ctx ATerm [ATerm]))
-> Sem (Error TCError : r) (Ctx ATerm [ATerm])
-> Sem r (Ctx ATerm [ATerm])
forall a b. (a -> b) -> a -> b
$ Ctx Term Docs -> Sem (Error TCError : r) (Ctx ATerm [ATerm])
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Error TCError,
    Fresh, Output Message]
  r =>
Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docCtx  -- XXX location?
          [(ATerm, PolyType)]
aterms <- (TCError -> LocTCError)
-> Sem (Error TCError : r) [(ATerm, PolyType)]
-> Sem r [(ATerm, PolyType)]
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError TCError -> LocTCError
noLoc (Sem (Error TCError : r) [(ATerm, PolyType)]
 -> Sem r [(ATerm, PolyType)])
-> Sem (Error TCError : r) [(ATerm, PolyType)]
-> Sem r [(ATerm, PolyType)]
forall a b. (a -> b) -> a -> b
$ (Term -> Sem (Error TCError : r) (ATerm, PolyType))
-> [Term] -> Sem (Error TCError : r) [(ATerm, PolyType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Sem (Error TCError : r) (ATerm, PolyType)
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader (Map String TyDefBody),
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop [Term]
terms     -- XXX location?
          ModuleInfo -> Sem r ModuleInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleInfo -> Sem r ModuleInfo) -> ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ ModuleName
-> Map ModuleName ModuleInfo
-> [QName Term]
-> Ctx Term Docs
-> Ctx ATerm [ATerm]
-> TyCtx
-> Map String TyDefBody
-> Ctx ATerm Defn
-> [(ATerm, PolyType)]
-> Set Ext
-> ModuleInfo
ModuleInfo ModuleName
name Map ModuleName ModuleInfo
imports ((TypeDecl -> QName Term) -> [TypeDecl] -> [QName Term]
forall a b. (a -> b) -> [a] -> [b]
map ((ModuleName
name ModuleName -> Name Term -> QName Term
forall a. ModuleName -> Name a -> QName a
.-) (Name Term -> QName Term)
-> (TypeDecl -> Name Term) -> TypeDecl -> QName Term
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 Map String TyDefBody
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 :: [TypeDefn] -> Sem r (Map String TyDefBody)
makeTyDefnCtx [TypeDefn]
tydefs = do
  Map String TyDefBody
oldTyDefs <- forall (r :: EffectRow).
Member (Reader (Map String TyDefBody)) r =>
Sem r (Map String TyDefBody)
forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  let oldNames :: [String]
oldNames = Map String TyDefBody -> [String]
forall k a. Map k a -> [k]
M.keys Map String TyDefBody
oldTyDefs
      newNames :: [String]
newNames = (TypeDefn -> String) -> [TypeDefn] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(TypeDefn String
x [String]
_ Type
_) -> String
x) [TypeDefn]
tydefs
      dups :: [String]
dups = [String] -> [String]
forall a. Ord a => [a] -> [a]
filterDups ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
newNames [String] -> [String] -> [String]
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 (([(Name Type, Type)] -> Type -> Type)
-> Type -> [(Name Type, Type)] -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(Name Type, Type)] -> Type -> Type
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs Type
body ([(Name Type, Type)] -> Type)
-> ([Type] -> [(Name Type, Type)]) -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name Type] -> [Type] -> [(Name Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((String -> Name Type) -> [String] -> [Name Type]
forall a b. (a -> b) -> [a] -> [b]
map String -> Name Type
forall a. String -> Name a
string2Name [String]
args)))

  case [String]
dups of
    (String
x:[String]
_) -> TCError -> Sem r (Map String TyDefBody)
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> TCError
DuplicateTyDefns String
x)
    []    -> Map String TyDefBody -> Sem r (Map String TyDefBody)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map String TyDefBody -> Sem r (Map String TyDefBody))
-> ([(String, TyDefBody)] -> Map String TyDefBody)
-> [(String, TyDefBody)]
-> Sem r (Map String TyDefBody)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, TyDefBody)] -> Map String TyDefBody
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, TyDefBody)] -> Sem r (Map String TyDefBody))
-> [(String, TyDefBody)] -> Sem r (Map String TyDefBody)
forall a b. (a -> b) -> a -> b
$ (TypeDefn -> (String, TyDefBody))
-> [TypeDefn] -> [(String, TyDefBody)]
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 :: ModuleName -> TypeDefn -> Sem r ()
checkTyDefn ModuleName
name defn :: TypeDefn
defn@(TypeDefn String
x [String]
args Type
body) = (TCError -> LocTCError) -> Sem (Error TCError : r) () -> Sem r ()
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 (QName Term -> Maybe (QName Term)
forall a. a -> Maybe a
Just (ModuleName
name ModuleName -> Name Term -> QName Term
forall a. ModuleName -> Name a -> QName a
.- String -> Name Term
forall a. String -> Name a
string2Name String
x))) (Sem (Error TCError : r) () -> Sem r ())
-> Sem (Error TCError : r) () -> Sem r ()
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.
  Type -> Sem (Error TCError : r) ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), 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
_ <- Type -> Set String -> Sem (Error TCError : r) (Set String)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy (String -> [Type] -> Type
TyUser String
x ((String -> Type) -> [String] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar (Name Type -> Type) -> (String -> Name Type) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name Type
forall a. String -> Name a
string2Name) [String]
args)) Set String
forall a. Set a
S.empty

  -- Make sure it does not use any unbound type variables or undefined
  -- types.
  TypeDefn -> Sem (Error TCError : r) ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), 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).
  TypeDefn -> Sem (Error TCError : r) ()
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 :: Type -> Set String -> Sem r (Set String)
checkCyclicTy (TyUser String
name [Type]
args) Set String
set = do
  case String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member String
name Set String
set of
    Bool
True -> TCError -> Sem r (Set String)
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r (Set String)) -> TCError -> Sem r (Set String)
forall a b. (a -> b) -> a -> b
$ String -> TCError
CyclicTyDef String
name
    Bool
False -> do
      Type
ty <- String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args
      Type -> Set String -> Sem r (Set String)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy Type
ty (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
S.insert String
name Set String
set)

checkCyclicTy Type
_ Set String
set = Set String -> Sem r (Set String)
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 :: 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)))
      | Name Type -> String
forall a. Name a -> String
name2String Name Type
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
args = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Bool
otherwise                 = TCError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r ()) -> TCError -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Name Type -> TCError
UnboundTyVar Name Type
x
    go (TyAtom Atom
_)        = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    go (TyUser String
name [Type]
tys) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
tys Sem r Type -> Sem r () -> Sem r ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type -> Sem r ()) -> [Type] -> Sem r ()
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)     = (Type -> Sem r ()) -> [Type] -> Sem r ()
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 :: 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 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name Bool -> Bool -> Bool
&& Bool -> Bool
not ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTyVar [Type]
tys) =
        TCError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r ()) -> TCError -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [Type] -> TCError
NoPolyRec String
name [String]
args [Type]
tys
      | Bool
otherwise = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    go (TyCon Con
_ [Type]
tys) = (Type -> Sem r ()) -> [Type] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Sem r ()
go [Type]
tys
    go Type
_             = () -> Sem r ()
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 :: [a] -> [a]
filterDups = ([a] -> a) -> [[a]] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> a
forall a. [a] -> a
head ([[a]] -> [a]) -> ([a] -> [[a]]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
1) (Int -> Bool) -> ([a] -> Int) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[a]] -> [[a]]) -> ([a] -> [[a]]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [[a]]
forall a. Eq a => [a] -> [[a]]
group ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
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 :: ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx ModuleName
name [TypeDecl]
decls = do
  let dups :: [Name Term]
dups = [Name Term] -> [Name Term]
forall a. Ord a => [a] -> [a]
filterDups ([Name Term] -> [Name Term])
-> ([TypeDecl] -> [Name Term]) -> [TypeDecl] -> [Name Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeDecl -> Name Term) -> [TypeDecl] -> [Name Term]
forall a b. (a -> b) -> [a] -> [b]
map (\(TypeDecl Name Term
x PolyType
_) -> Name Term
x) ([TypeDecl] -> [Name Term]) -> [TypeDecl] -> [Name Term]
forall a b. (a -> b) -> a -> b
$ [TypeDecl]
decls
  case [Name Term]
dups of
    (Name Term
x:[Name Term]
_) -> TCError -> Sem r TyCtx
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
DuplicateDecls Name Term
x)
    []    -> do
      TyCtx -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
TyCtx -> Sem r ()
checkCtx TyCtx
declCtx
      TyCtx -> Sem r TyCtx
forall (m :: * -> *) a. Monad m => a -> m a
return TyCtx
declCtx
  where
    declCtx :: TyCtx
declCtx = ModuleName -> [(Name Term, PolyType)] -> TyCtx
forall a b. ModuleName -> [(Name a, b)] -> Ctx a b
ctxForModule ModuleName
name ([(Name Term, PolyType)] -> TyCtx)
-> [(Name Term, PolyType)] -> TyCtx
forall a b. (a -> b) -> a -> b
$ (TypeDecl -> (Name Term, PolyType))
-> [TypeDecl] -> [(Name Term, PolyType)]
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 :: TyCtx -> Sem r ()
checkCtx = (PolyType -> Sem r ()) -> [PolyType] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PolyType -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid ([PolyType] -> Sem r ())
-> (TyCtx -> [PolyType]) -> TyCtx -> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCtx -> [PolyType]
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] r
  => ModuleName -> TermDefn -> Sem r Defn
checkDefn :: ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name (TermDefn Name Term
x [Bind [Pattern] Term]
clauses) = (TCError -> LocTCError)
-> Sem (Error TCError : r) Defn -> Sem r Defn
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 (QName Term -> Maybe (QName Term)
forall a. a -> Maybe a
Just (ModuleName
name ModuleName -> Name Term -> QName Term
forall a. ModuleName -> Name a -> QName a
.- Name Term
x))) (Sem (Error TCError : r) Defn -> Sem r Defn)
-> Sem (Error TCError : r) Defn -> Sem r Defn
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 <- QName Term -> Sem (Error TCError : r) (Maybe PolyType)
forall a b (r :: EffectRow).
Member (Reader (Ctx a b)) r =>
QName a -> Sem r (Maybe b)
lookup (ModuleName
name ModuleName -> Name Term -> QName Term
forall a. ModuleName -> Name a -> QName a
.- Name Term
x) Sem (Error TCError : r) (Maybe PolyType)
-> (Maybe PolyType -> Sem (Error TCError : r) PolyType)
-> Sem (Error TCError : r) PolyType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sem (Error TCError : r) PolyType
-> (PolyType -> Sem (Error TCError : r) PolyType)
-> Maybe PolyType
-> Sem (Error TCError : r) PolyType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TCError -> Sem (Error TCError : r) PolyType
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem (Error TCError : r) PolyType)
-> TCError -> Sem (Error TCError : r) PolyType
forall a b. (a -> b) -> a -> b
$ Name Term -> TCError
NoType Name Term
x) PolyType -> Sem (Error TCError : r) PolyType
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) <- Bind [Name Type] Type
-> Sem (Error TCError : r) ([Name Type], Type)
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) <- Int -> Type -> Sem (Error TCError : r) ([Type], Type)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Bind [Pattern] Term -> Int
numPats ([Bind [Pattern] Term] -> Bind [Pattern] Term
forall a. [a] -> a
head [Bind [Pattern] Term]
clauses)) Type
ty

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

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

    checkNumPats :: [Bind [Pattern] Term] -> Sem (Error TCError : r) ()
checkNumPats []     = () -> Sem (Error TCError : r) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- This can't happen, but meh
    checkNumPats [Bind [Pattern] Term
_]    = () -> Sem (Error TCError : r) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkNumPats (Bind [Pattern] Term
c:[Bind [Pattern] Term]
cs)
      | (Bind [Pattern] Term -> Bool) -> [Bind [Pattern] Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0) (Int -> Bool)
-> (Bind [Pattern] Term -> Int) -> Bind [Pattern] Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term -> Int
numPats) (Bind [Pattern] Term
cBind [Pattern] Term
-> [Bind [Pattern] Term] -> [Bind [Pattern] Term]
forall a. a -> [a] -> [a]
:[Bind [Pattern] Term]
cs) = TCError -> Sem (Error TCError : r) ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
DuplicateDefns Name Term
x)
      | Bool -> Bool
not ((Bind [Pattern] Term -> Bool) -> [Bind [Pattern] Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Bind [Pattern] Term -> Int
numPats Bind [Pattern] Term
c) (Int -> Bool)
-> (Bind [Pattern] Term -> Int) -> Bind [Pattern] Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term -> Int
numPats) [Bind [Pattern] Term]
cs) = TCError -> Sem (Error TCError : r) ()
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 = () -> Sem (Error TCError : r) ()
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 :: [Type] -> Type -> Bind [Pattern] Term -> Sem r Clause
checkClause [Type]
patTys Type
bodyTy Bind [Pattern] Term
clause = do
      ([Pattern]
pats, Term
body) <- Bind [Pattern] Term -> Sem r ([Pattern], Term)
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) <- [(TyCtx, APattern)] -> ([TyCtx], [APattern])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(TyCtx, APattern)] -> ([TyCtx], [APattern]))
-> Sem r [(TyCtx, APattern)] -> Sem r ([TyCtx], [APattern])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> Type -> Sem r (TyCtx, APattern))
-> [Pattern] -> [Type] -> Sem r [(TyCtx, APattern)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern [Pattern]
pats [Type]
patTys
      ATerm
at  <- TyCtx -> Sem r ATerm -> Sem r ATerm
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. Monoid a => [a] -> a
mconcat [TyCtx]
ctxs) (Sem r ATerm -> Sem r ATerm) -> Sem r ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
body Type
bodyTy
      Clause -> Sem r Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> Sem r Clause) -> Clause -> Sem r Clause
forall a b. (a -> b) -> a -> b
$ [APattern] -> ATerm -> Clause
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 :: Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
0 Type
ty = ([Type], Type) -> Sem r ([Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
ty)
    decomposeDefnTy Int
n (TyUser String
tyName [Type]
args) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
tyName [Type]
args Sem r Type
-> (Type -> Sem r ([Type], Type)) -> Sem r ([Type], Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Type -> Sem r ([Type], Type)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
n
    decomposeDefnTy Int
n (Type
ty1 :->: Type
ty2) = ([Type] -> [Type]) -> ([Type], Type) -> ([Type], Type)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type
ty1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:) (([Type], Type) -> ([Type], Type))
-> Sem r ([Type], Type) -> Sem r ([Type], Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Type -> Sem r ([Type], Type)
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Type
ty2
    decomposeDefnTy Int
_n Type
_ty = TCError -> Sem r ([Type], Type)
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] r
  => Ctx Term Docs -> Sem r (Ctx ATerm [AProperty])
checkProperties :: Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docs =
  Ctx Term [ATerm] -> Ctx ATerm [ATerm]
forall a1 b a2. Ctx a1 b -> Ctx a2 b
Ctx.coerceKeys (Ctx Term [ATerm] -> Ctx ATerm [ATerm])
-> (Ctx Term [ATerm] -> Ctx Term [ATerm])
-> Ctx Term [ATerm]
-> Ctx ATerm [ATerm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ATerm] -> Bool) -> Ctx Term [ATerm] -> Ctx Term [ATerm]
forall b a. (b -> Bool) -> Ctx a b -> Ctx a b
Ctx.filter (Bool -> Bool
not (Bool -> Bool) -> ([ATerm] -> Bool) -> [ATerm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ATerm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null)
    (Ctx Term [ATerm] -> Ctx ATerm [ATerm])
-> Sem r (Ctx Term [ATerm]) -> Sem r (Ctx ATerm [ATerm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Term] -> Sem r [ATerm])
-> Ctx Term [Term] -> Sem r (Ctx Term [ATerm])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (([Term] -> Sem r [ATerm])
 -> Ctx Term [Term] -> Sem r (Ctx Term [ATerm]))
-> ((Term -> Sem r ATerm) -> [Term] -> Sem r [ATerm])
-> (Term -> Sem r ATerm)
-> Ctx Term [Term]
-> Sem r (Ctx Term [ATerm])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Sem r ATerm) -> [Term] -> Sem r [ATerm]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Error TCError,
    Fresh, Output Message]
  r =>
Term -> Sem r ATerm
checkProperty Ctx Term [Term]
properties
  where
    properties :: Ctx Term [Property]
    properties :: Ctx Term [Term]
properties = (Docs -> [Term]) -> Ctx Term Docs -> Ctx Term [Term]
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] r
  => Property -> Sem r AProperty
checkProperty :: Term -> Sem r ATerm
checkProperty Term
prop = do
  (ATerm
at, S
theta) <- Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall (r :: EffectRow) a.
Members
  '[Reader (Map String TyDefBody), Error TCError, Output Message]
  r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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?
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ S -> ATerm -> ATerm
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 :: PolyType -> Sem r ()
checkPolyTyValid (Forall Bind [Name Type] Type
b) = do
  let ([Name Type]
_, Type
ty) = Bind [Name Type] Type -> ([Name Type], Type)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind Bind [Name Type] Type
b
  Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), 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 :: Type -> Sem r ()
checkTypeValid (TyAtom Atom
_)    = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkTypeValid (TyCon Con
c [Type]
tys) = do
  Int
k <- Con -> Sem r Int
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Con -> Sem r Int
conArity Con
c
  if | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k     -> TCError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> TCError
NotEnoughArgs Con
c)
     | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
k     -> TCError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Con -> TCError
TooManyArgs Con
c)
     | Bool
otherwise -> (Type -> Sem r ()) -> [Type] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Sem r ()
checkTypeValid [Type]
tys
  where
    n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys

conArity :: Members '[Reader TyDefCtx, Error TCError] r => Con -> Sem r Int
conArity :: Con -> Sem r Int
conArity (CContainer Atom
_) = Int -> Sem r Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity Con
CGraph = Int -> Sem r Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity (CUser String
name)    = do
  Map String TyDefBody
d <- forall (r :: EffectRow).
Member (Reader (Map String TyDefBody)) r =>
Sem r (Map String TyDefBody)
forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  case String -> Map String TyDefBody -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name Map String TyDefBody
d of
    Maybe TyDefBody
Nothing               -> TCError -> Sem r Int
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
_) -> Int -> Sem r Int
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
as)
conArity Con
_              = Int -> Sem r Int
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
(Int -> Mode -> ShowS)
-> (Mode -> String) -> ([Mode] -> ShowS) -> Show Mode
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 :: Term -> Type -> Sem r ATerm
check Term
t Type
ty = Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 :: Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t (Forall Bind [Name Type] Type
sig) = do
  ([Name Type]
as, Type
tau) <- Bind [Name Type] Type -> Sem r ([Name Type], Type)
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) <- Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, Constraint)
forall (r :: EffectRow) a.
Sem (Writer Constraint : r) a -> Sem r (a, Constraint)
withConstraint (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, Constraint))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, Constraint)
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
tau
  case [Name Type]
as of
    [] -> Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint Constraint
cst
    [Name Type]
_  -> Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Bind [Name Type] Constraint -> Constraint
CAll ([Name Type] -> Constraint -> Bind [Name Type] Constraint
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Name Type]
as Constraint
cst)
  ATerm -> Sem r ATerm
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 :: Term -> Sem r ATerm
infer = Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r
  => Term -> Sem r (ATerm, PolyType)
inferTop :: 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) <- Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall (r :: EffectRow) a.
Members
  '[Reader (Map String TyDefBody), Error TCError, Output Message]
  r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall a b. (a -> b) -> a -> b
$ Term -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t

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

      -- Apply the resulting substitution.
  let at' :: ATerm
at' = S -> ATerm -> ATerm
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 (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at')

      -- Replace them all with List.
      at'' :: ATerm
at'' = S -> ATerm -> ATerm
forall b a. Subst b a => Substitution b -> a -> a
applySubst ([(Name Type, Type)] -> S
forall a. [(Name a, a)] -> Substitution a
Subst.fromList ([(Name Type, Type)] -> S) -> [(Name Type, Type)] -> S
forall a b. (a -> b) -> a -> b
$ [Name Type] -> [Type] -> [(Name Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set (Name Type) -> [Name Type]
forall a. Set a -> [a]
S.toList Set (Name Type)
cvs) (Type -> [Type]
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.
  (ATerm, PolyType) -> Sem r (ATerm, PolyType)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm
at'', Type -> PolyType
closeType (ATerm -> Type
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, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r
  => Term -> PolyType -> Sem r ATerm
checkTop :: Term -> PolyType -> Sem r ATerm
checkTop Term
t PolyType
ty = do
  (ATerm
at, S
theta) <- Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall (r :: EffectRow) a.
Members
  '[Reader (Map String TyDefBody), Error TCError, Output Message]
  r =>
Sem (Writer Constraint : r) a -> Sem r (a, S)
solve (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, S)
forall a b. (a -> b) -> a -> b
$ Term -> PolyType -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t PolyType
ty
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ S -> ATerm -> ATerm
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 :: Mode -> Term -> Sem r ATerm
typecheck (Check (TyUser String
name [Type]
args)) Term
t = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args Sem r Type -> (Type -> Sem r ATerm) -> Sem r ATerm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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) = Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 <- MaybeT (Sem r) ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (Sem r) ATerm -> Sem r (Maybe ATerm))
-> ([Sem r (Maybe ATerm)] -> MaybeT (Sem r) ATerm)
-> [Sem r (Maybe ATerm)]
-> Sem r (Maybe ATerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MaybeT (Sem r) ATerm] -> MaybeT (Sem r) ATerm
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum ([MaybeT (Sem r) ATerm] -> MaybeT (Sem r) ATerm)
-> ([Sem r (Maybe ATerm)] -> [MaybeT (Sem r) ATerm])
-> [Sem r (Maybe ATerm)]
-> MaybeT (Sem r) ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sem r (Maybe ATerm) -> MaybeT (Sem r) ATerm)
-> [Sem r (Maybe ATerm)] -> [MaybeT (Sem r) ATerm]
forall a b. (a -> b) -> [a] -> [b]
map Sem r (Maybe ATerm) -> MaybeT (Sem r) ATerm
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT ([Sem r (Maybe ATerm)] -> Sem r (Maybe ATerm))
-> [Sem r (Maybe ATerm)] -> Sem r (Maybe ATerm)
forall a b. (a -> b) -> a -> b
$ [Sem r (Maybe ATerm)
tryLocal, Sem r (Maybe ATerm)
tryModule, Sem r (Maybe ATerm)
tryPrim]
  Sem r ATerm -> (ATerm -> Sem r ATerm) -> Maybe ATerm -> Sem r ATerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TCError -> Sem r ATerm
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (Name Term -> TCError
Unbound Name Term
x)) ATerm -> Sem r ATerm
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 <- QName Term -> Sem r (Maybe PolyType)
forall a b (r :: EffectRow).
Member (Reader (Ctx a b)) r =>
QName a -> Sem r (Maybe b)
Ctx.lookup (Name Term -> QName Term
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) <- Bind [Name Type] Type -> Sem r ([Name Type], Type)
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
          Maybe ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ATerm -> Sem r (Maybe ATerm))
-> (ATerm -> Maybe ATerm) -> ATerm -> Sem r (Maybe ATerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Maybe ATerm
forall a. a -> Maybe a
Just (ATerm -> Sem r (Maybe ATerm)) -> ATerm -> Sem r (Maybe ATerm)
forall a b. (a -> b) -> a -> b
$ Type -> QName ATerm -> ATerm
ATVar Type
ty (Name ATerm -> QName ATerm
forall a. Name a -> QName a
localName (Name Term -> Name ATerm
coerce Name Term
x))
        Maybe PolyType
Nothing -> Maybe ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ATerm
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 <- Name Term -> Sem r [(ModuleName, PolyType)]
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) <- Bind [Name Type] Type -> Sem r ([Name Type], Type)
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
          Maybe ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ATerm -> Sem r (Maybe ATerm))
-> (ATerm -> Maybe ATerm) -> ATerm -> Sem r (Maybe ATerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Maybe ATerm
forall a. a -> Maybe a
Just (ATerm -> Sem r (Maybe ATerm)) -> ATerm -> Sem r (Maybe ATerm)
forall a b. (a -> b) -> a -> b
$ Type -> QName ATerm -> ATerm
ATVar Type
ty (ModuleName
m ModuleName -> Name ATerm -> QName ATerm
forall a. ModuleName -> Name a -> QName a
.- Name Term -> Name ATerm
coerce Name Term
x)
        []       -> Maybe ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ATerm
forall a. Maybe a
Nothing
        [(ModuleName, PolyType)]
_        -> TCError -> Sem r (Maybe ATerm)
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r (Maybe ATerm)) -> TCError -> Sem r (Maybe ATerm)
forall a b. (a -> b) -> a -> b
$ Name Term -> [ModuleName] -> TCError
Ambiguous Name Term
x (((ModuleName, PolyType) -> ModuleName)
-> [(ModuleName, PolyType)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, PolyType) -> ModuleName
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 (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) of
        (Prim
prim:[Prim]
_) -> ATerm -> Maybe ATerm
forall a. a -> Maybe a
Just (ATerm -> Maybe ATerm) -> Sem r ATerm -> Sem r (Maybe ATerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
Infer (Prim -> Term
TPrim Prim
prim)
        [Prim]
_        -> Maybe ATerm -> Sem r (Maybe ATerm)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ATerm
forall a. Maybe a
Nothing

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

typecheck Mode
Infer (TPrim Prim
prim) = do
  Type
ty <- Prim -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Prim -> Sem r Type
inferPrim Prim
prim
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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 :: Prim -> Sem r Type
inferPrim Prim
PrimLeft = do
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
b Type -> Type -> Type
:->: (Type
a Type -> Type -> Type
:+: Type
b)

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

    --- XXX restore typing rules for logical operations on Props
    --- once the evaluator can handle them.

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

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

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

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

    inferPrim Prim
conv | Prim
conv Prim -> [Prim] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prim
PrimList, Prim
PrimBag, Prim
PrimSet] = do
      Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom   -- make a unification variable for the container type
      Type
a <- Sem r Type
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
      Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Prim
conv Prim -> Prim -> Bool
forall a. Eq a => a -> a -> Bool
/= Prim
PrimList) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a

      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim PrimList should be unreachable"
    inferPrim Prim
PrimBag  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim PrimBag should be unreachable"
    inferPrim Prim
PrimSet  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim PrimSet should be unreachable"
    ------------------------------------------------------------

    inferPrim Prim
PrimB2C = do
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
v <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
k
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
v <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
k
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
a Type -> Type -> Type
:->: Type -> Type
TyGraph Type
a

    inferPrim Prim
PrimEmptyGraph = do
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
TyGraph Type
a

    inferPrim Prim
PrimOverlay = do
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSimple Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
b <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Union, BOp
Inter, BOp
Diff, BOp
Subset] = do
      Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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}
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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)  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Union should be unreachable"
    inferPrim (PrimBOp BOp
Inter)  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Inter should be unreachable"
    inferPrim (PrimBOp BOp
Diff)   = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Diff should be unreachable"
    inferPrim (PrimBOp BOp
Subset) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Subset should be unreachable"
    ------------------------------------------------------------

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

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

      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type
resTy <- Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
a Type
TyZ
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 BOp -> [BOp] -> Bool
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual (BOp -> Qualifier
bopQual BOp
op) Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 ) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Add should be unreachable"
    inferPrim (PrimBOp BOp
Mul ) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Mul should be unreachable"
    inferPrim (PrimBOp BOp
Sub ) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Sub should be unreachable"
    inferPrim (PrimBOp BOp
Div ) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Div should be unreachable"
    inferPrim (PrimBOp BOp
SSub) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim SSub should be unreachable"
    ------------------------------------------------------------

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

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

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

    inferPrim Prim
PrimIsPrime = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyBool
    inferPrim Prim
PrimFactor  = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type -> Type
TyBag Type
TyN

    inferPrim Prim
PrimFrac    = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
a
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
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).
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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)]
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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   = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 BOp -> [BOp] -> Bool
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
ty
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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)  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Eq should be unreachable"
    inferPrim (PrimBOp BOp
Neq) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Neq should be unreachable"
    inferPrim (PrimBOp BOp
Lt)  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Lt should be unreachable"
    inferPrim (PrimBOp BOp
Gt)  = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Gt should be unreachable"
    inferPrim (PrimBOp BOp
Leq) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Leq should be unreachable"
    inferPrim (PrimBOp BOp
Geq) = String -> Sem r Type
forall a. HasCallStack => String -> a
error String
"inferPrim Geq should be unreachable"
    ------------------------------------------------------------

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

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

    inferPrim (PrimUOp UOp
Fact) = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyN
    inferPrim Prim
PrimSqrt = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Type
TyN Type -> Type -> Type
:->: Type
TyN

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

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

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

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

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

      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
a
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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)
        ]

      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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        = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return ATerm
ATUnit
typecheck Mode
Infer             (TBool Bool
b)    = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> Bool -> ATerm
ATBool Type
TyBool Bool
b
typecheck Mode
Infer             (TChar Char
c)    = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Char -> ATerm
ATChar Char
c
typecheck Mode
Infer             (TString String
cs) = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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)     = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> Integer -> ATerm
ATNat Type
TyN Integer
n
typecheck Mode
Infer             (TRat Rational
r)     = ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Rational -> ATerm
ATRat Rational
r

typecheck Mode
_                 Term
TWild        = TCError -> Sem r ATerm
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) <- Bind [Pattern] Term -> Sem r ([Pattern], Term)
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) <- [Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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.
  TyCtx -> Sem r ATerm -> Sem r ATerm
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx (Sem r ATerm -> Sem r ATerm) -> Sem r ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$
    Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
Lam Type
checkTy (Clause -> ATerm) -> Sem r Clause -> Sem r ATerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([APattern] -> ATerm -> Clause
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([APattern] -> [APattern]
coerce [APattern]
typedArgs) (ATerm -> Clause) -> Sem r ATerm -> Sem r Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 :: [Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [] Type
ty Term
_ = (TyCtx, [APattern], Type) -> Sem r (TyCtx, [APattern], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
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) <- Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CArr Type
ty (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Term
term)

      -- Check the argument pattern against the function domain.
      (TyCtx
pCtx, APattern
pTyped) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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) <- [Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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.
      (TyCtx, [APattern], Type) -> Sem r (TyCtx, [APattern], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
pCtx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ctx, APattern
pTyped APattern -> [APattern] -> [APattern]
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) <- Bind [Pattern] Term -> Sem r ([Pattern], Term)
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 <- (Pattern -> Sem r Type) -> [Pattern] -> Sem r [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Pattern -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError, Fresh] r =>
Pattern -> Sem r Type
getAscrOrFresh [Pattern]
args
  ([TyCtx]
pCtxs, [APattern]
typedPats) <- [(TyCtx, APattern)] -> ([TyCtx], [APattern])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(TyCtx, APattern)] -> ([TyCtx], [APattern]))
-> Sem r [(TyCtx, APattern)] -> Sem r ([TyCtx], [APattern])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> Type -> Sem r (TyCtx, APattern))
-> [Pattern] -> [Type] -> Sem r [(TyCtx, APattern)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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.
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Quantifier
q Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Quantifier
All, Quantifier
Ex]) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
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.
    [Type] -> (Type -> Sem r ()) -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((APattern -> Type) -> [APattern] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Type
forall t. HasType t => t -> Type
getType [APattern]
typedPats) ((Type -> Sem r ()) -> Sem r ()) -> (Type -> Sem r ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
      Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
isSearchable Type
ty) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$
        TCError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r ()) -> TCError -> Sem r ()
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.
  TyCtx -> Sem r ATerm -> Sem r ATerm
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. Monoid a => [a] -> a
mconcat [TyCtx]
pCtxs) (Sem r ATerm -> Sem r ATerm) -> Sem r ATerm -> Sem r ATerm
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 <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
        ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
Lam ([Type] -> Type -> Type
mkFunTy [Type]
tys (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at)) ([APattern] -> ATerm -> Clause
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 <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
TyProp
        ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Quantifier -> Type -> Clause -> ATerm
ATAbs Quantifier
q Type
TyProp ([APattern] -> ATerm -> Clause
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 :: Pattern -> Sem r Type
getAscrOrFresh (PAscr Pattern
_ Type
ty) = Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
ty Sem r () -> Sem r Type -> Sem r Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> Sem r Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
    getAscrOrFresh Pattern
_            = Sem r Type
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 = (Type -> Type -> Type) -> Type -> [Type] -> Type
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 <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
  let ty :: Type
ty = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at
  (Type
ty1, Type
ty2) <- Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CArr Type
ty (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Term
t)
  Type -> ATerm -> ATerm -> ATerm
ATApp Type
ty2 ATerm
at (ATerm -> ATerm) -> Sem r ATerm -> Sem r ATerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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) = (Type -> [ATerm] -> ATerm) -> (Type, [ATerm]) -> ATerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> [ATerm] -> ATerm
ATTup ((Type, [ATerm]) -> ATerm) -> Sem r (Type, [ATerm]) -> Sem r ATerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> [Term] -> Sem r (Type, [ATerm])
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 :: Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
_    []     = String -> Sem r (Type, [ATerm])
forall a. HasCallStack => String -> a
error String
"Impossible! typecheckTuple []"
    typecheckTuple Mode
mode [Term
t]    = (ATerm -> Type
forall t. HasType t => t -> Type
getType (ATerm -> Type) -> (ATerm -> [ATerm]) -> ATerm -> (Type, [ATerm])
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (ATerm -> [ATerm] -> [ATerm]
forall a. a -> [a] -> [a]
:[])) (ATerm -> (Type, [ATerm])) -> Sem r ATerm -> Sem r (Type, [ATerm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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)    <- Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
CProd Mode
mode (Term -> Either Term Pattern
forall a b. a -> Either a b
Left (Term -> Either Term Pattern) -> Term -> Either Term Pattern
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
TTup (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
ts))
      ATerm
at        <- Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck      Mode
m  Term
t
      (Type
ty, [ATerm]
ats) <- Mode -> [Term] -> Sem r (Type, [ATerm])
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
ms [Term]
ts
      (Type, [ATerm]) -> Sem r (Type, [ATerm])
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at Type -> Type -> Type
:*: Type
ty, ATerm
at ATerm -> [ATerm] -> [ATerm]
forall a. a -> [a] -> [a]
: [ATerm]
ats)

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

typecheck Mode
Infer (TChain Term
t [Link]
ls) =
  Type -> ATerm -> [ALink] -> ATerm
ATChain Type
TyBool (ATerm -> [ALink] -> ATerm)
-> Sem r ATerm -> Sem r ([ALink] -> ATerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t Sem r ([ALink] -> ATerm) -> Sem r [ALink] -> Sem r ATerm
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> [Link] -> Sem r [ALink]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> [Link] -> Sem r [ALink]
inferChain Term
t [Link]
ls

  where
    inferChain
      :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r
      => Term -> [Link] -> Sem r [ALink]
    inferChain :: Term -> [Link] -> Sem r [ALink]
inferChain Term
_  [] = [ALink] -> Sem r [ALink]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    inferChain Term
t1 (TLink BOp
op Term
t2 : [Link]
links) = do
      ATerm
at2 <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t2
      ATerm
_   <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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
      [ALink]
atl <- Term -> [Link] -> Sem r [ALink]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> [Link] -> Sem r [ALink]
inferChain Term
t2 [Link]
links
      [ALink] -> Sem r [ALink]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ALink] -> Sem r [ALink]) -> [ALink] -> Sem r [ALink]
forall a b. (a -> b) -> a -> b
$ BOp -> ATerm -> ALink
ATLink BOp
op ATerm
at2 ALink -> [ALink] -> [ALink]
forall a. a -> [a] -> [a]
: [ALink]
atl

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

typecheck Mode
Infer (TTyOp TyOp
Enumerate Type
t) = do
  Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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
  Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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 <- Con -> Mode -> Either Term Pattern -> Sem r Mode
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 (Container -> Con
containerToCon Container
c) Mode
mode (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Term
t)
  [(ATerm, Maybe ATerm)]
axns  <- ((Term, Maybe Term) -> Sem r (ATerm, Maybe ATerm))
-> [(Term, Maybe Term)] -> Sem r [(ATerm, Maybe ATerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Term
x,Maybe Term
n) -> (,) (ATerm -> Maybe ATerm -> (ATerm, Maybe ATerm))
-> Sem r ATerm -> Sem r (Maybe ATerm -> (ATerm, Maybe ATerm))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
eltMode Term
x Sem r (Maybe ATerm -> (ATerm, Maybe ATerm))
-> Sem r (Maybe ATerm) -> Sem r (ATerm, Maybe ATerm)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> Sem r ATerm) -> Maybe Term -> Sem r (Maybe ATerm)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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  <- Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 = [ ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at | Just (Until ATerm
at) <- [Maybe (Ellipsis ATerm)
aell] ] [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ ((ATerm, Maybe ATerm) -> Type) -> [(ATerm, Maybe ATerm)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (ATerm -> Type
forall t. HasType t => t -> Type
getType (ATerm -> Type)
-> ((ATerm, Maybe ATerm) -> ATerm) -> (ATerm, Maybe ATerm) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, Maybe ATerm) -> ATerm
forall a b. (a, b) -> a
fst) [(ATerm, Maybe ATerm)]
axns
      Type
tyv  <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      [Constraint] -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
[Constraint] -> Sem r ()
constraints ([Constraint] -> Sem r ()) -> [Constraint] -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (Type -> Constraint) -> [Type] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type -> Constraint
`CSub` Type
tyv) [Type]
tys
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
forall a b. (a -> b) -> a -> b
$ Container -> Type -> Type
containerTy Container
c Type
tyv
    Check Type
ty -> Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
  Type
eltTy <- Container -> Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Container -> Type -> Sem r Type
getEltTy Container
c Type
resTy

  -- See Note [Container literal constraints]
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Container
c Container -> Container -> Bool
forall a. Eq a => a -> a -> Bool
/= Container
ListContainer Bool -> Bool -> Bool
&& Bool -> Bool
not ([(Term, Maybe Term)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(Term, Maybe Term)]
xs)) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QCmp Type
eltTy
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe (Ellipsis Term) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Ellipsis Term)
ell) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QEnum Type
eltTy
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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 :: Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
typecheckEllipsis Mode
_ Maybe (Ellipsis Term)
Nothing           = Maybe (Ellipsis ATerm) -> Sem r (Maybe (Ellipsis ATerm))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Ellipsis ATerm)
forall a. Maybe a
Nothing
    typecheckEllipsis Mode
m (Just (Until Term
tm)) = Ellipsis ATerm -> Maybe (Ellipsis ATerm)
forall a. a -> Maybe a
Just (Ellipsis ATerm -> Maybe (Ellipsis ATerm))
-> (ATerm -> Ellipsis ATerm) -> ATerm -> Maybe (Ellipsis ATerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Ellipsis ATerm
forall t. t -> Ellipsis t
Until (ATerm -> Maybe (Ellipsis ATerm))
-> Sem r ATerm -> Sem r (Maybe (Ellipsis ATerm))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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) Term
bqt) = do
  Mode
eltMode <- Con -> Mode -> Either Term Pattern -> Sem r Mode
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 (Container -> Con
containerToCon Container
c) Mode
mode (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Term
tcc)
  (Telescope Qual
qs, Term
t)   <- Bind (Telescope Qual) Term -> Sem r (Telescope Qual, Term)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope Qual) Term
bqt
  (Telescope AQual
aqs, TyCtx
cx) <- (Qual -> Sem r (AQual, TyCtx))
-> Telescope Qual -> Sem r (Telescope AQual, TyCtx)
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 Qual -> Sem r (AQual, TyCtx)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Qual -> Sem r (AQual, TyCtx)
inferQual Telescope Qual
qs
  TyCtx -> Sem r ATerm -> Sem r ATerm
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
cx (Sem r ATerm -> Sem r ATerm) -> Sem r ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ do
    ATerm
at <- Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at)
          Check Type
ty -> Type
ty
    ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> Container -> Bind (Telescope AQual) ATerm -> ATerm
ATContainerComp Type
resTy Container
c (Telescope AQual -> ATerm -> Bind (Telescope AQual) ATerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope AQual
aqs ATerm
at)

  where
    inferQual
      :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r
      => Qual -> Sem r (AQual, TyCtx)
    inferQual :: Qual -> Sem r (AQual, TyCtx)
inferQual (QBind Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t))  = do
      ATerm
at <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
      Type
ty <- Con -> Type -> Either Term Pattern -> Sem r Type
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 (Container -> Con
containerToCon Container
c) (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at) (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Embedded (Embed Term)
Term
t)
      (AQual, TyCtx) -> Sem r (AQual, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Embed ATerm -> AQual
AQBind (Name Term -> Name ATerm
coerce Name Term
x) (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at), QName Term -> PolyType -> TyCtx
forall a b. QName a -> b -> Ctx a b
singleCtx (Name Term -> QName Term
forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType Type
ty))

    inferQual (QGuard (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t))   = do
      ATerm
at <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
Term
t Type
TyBool
      (AQual, TyCtx) -> Sem r (AQual, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> AQual
AQGuard (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at), TyCtx
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) Term
l) = do
  (Telescope Binding
bs, Term
t2) <- Bind (Telescope Binding) Term -> Sem r (Telescope Binding, Term)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope Binding) Term
l

  -- Infer the types of all the variables bound by the let...
  (Telescope ABinding
as, TyCtx
ctx) <- (Binding -> Sem r (ABinding, TyCtx))
-> Telescope Binding -> Sem r (Telescope ABinding, TyCtx)
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 Binding -> Sem r (ABinding, TyCtx)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Binding -> Sem r (ABinding, TyCtx)
inferBinding Telescope Binding
bs

  -- ...then check/infer the body under an extended context.
  TyCtx -> Sem r ATerm -> Sem r ATerm
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx (Sem r ATerm -> Sem r ATerm) -> Sem r ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ do
    ATerm
at2 <- Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t2
    ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> Bind (Telescope ABinding) ATerm -> ATerm
ATLet (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at2) (Telescope ABinding -> ATerm -> Bind (Telescope ABinding) ATerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope ABinding
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 :: Binding -> Sem r (ABinding, TyCtx)
inferBinding (Binding Maybe (Embed PolyType)
mty Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
      ATerm
at <- case Maybe (Embed PolyType)
mty of
        Just (Embed PolyType -> Embedded (Embed PolyType)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty) -> Term -> PolyType -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Embedded (Embed Term)
Term
t Embedded (Embed PolyType)
PolyType
ty
        Maybe (Embed PolyType)
Nothing              -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
      (ABinding, TyCtx) -> Sem r (ABinding, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> ABinding
ABinding Maybe (Embed PolyType)
mty (Name Term -> Name ATerm
coerce Name Term
x) (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at), QName Term -> PolyType -> TyCtx
forall a b. QName a -> b -> Ctx a b
singleCtx (Name Term -> QName Term
forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType (Type -> PolyType) -> Type -> PolyType
forall a b. (a -> b) -> a -> b
$ ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at))

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

-- Check/infer a case expression.
typecheck Mode
_    (TCase []) = TCError -> Sem r ATerm
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' <- (Branch -> Sem r ABranch) -> [Branch] -> Sem r [ABranch]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Branch -> Sem r ABranch
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Branch -> Sem r ABranch
typecheckBranch [Branch]
bs
  Type
resTy <- case Mode
mode of
    Check Type
ty -> Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    Mode
Infer    -> do
      Type
x <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
      [Constraint] -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
[Constraint] -> Sem r ()
constraints ([Constraint] -> Sem r ()) -> [Constraint] -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (ABranch -> Constraint) -> [ABranch] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type -> Constraint
`CSub` Type
x) (Type -> Constraint) -> (ABranch -> Type) -> ABranch -> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ABranch -> Type
forall t. HasType t => t -> Type
getType) [ABranch]
bs'
      Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
x
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
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 :: Branch -> Sem r ABranch
typecheckBranch Branch
b = do
      (Telescope (Guard_ UD)
gs, Term
t) <- Branch -> Sem r (Telescope (Guard_ UD), Term)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Branch
b
      (Telescope AGuard
ags, TyCtx
ctx) <- (Guard_ UD -> Sem r (AGuard, TyCtx))
-> Telescope (Guard_ UD) -> Sem r (Telescope AGuard, TyCtx)
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 Guard_ UD -> Sem r (AGuard, TyCtx)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Guard_ UD -> Sem r (AGuard, TyCtx)
inferGuard Telescope (Guard_ UD)
gs
      TyCtx -> Sem r ABranch -> Sem r ABranch
forall a b (r :: EffectRow) c.
Member (Reader (Ctx a b)) r =>
Ctx a b -> Sem r c -> Sem r c
extends TyCtx
ctx (Sem r ABranch -> Sem r ABranch) -> Sem r ABranch -> Sem r ABranch
forall a b. (a -> b) -> a -> b
$
        Telescope AGuard -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope AGuard
ags (ATerm -> ABranch) -> Sem r ATerm -> Sem r ABranch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 :: Guard_ UD -> Sem r (AGuard, TyCtx)
inferGuard (GBool (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)) = do
      ATerm
at <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
Term
t Type
TyBool
      (AGuard, TyCtx) -> Sem r (AGuard, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> AGuard
AGBool (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at), TyCtx
forall a b. Ctx a b
emptyCtx)
    inferGuard (GPat (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) Pattern
p) = do
      ATerm
at <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
      (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at)
      (AGuard, TyCtx) -> Sem r (AGuard, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> APattern -> AGuard
AGPat (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at) APattern
apt, TyCtx
ctx)
    inferGuard (GLet (Binding Maybe (Embed PolyType)
mty Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t))) = do
      ATerm
at <- case Maybe (Embed PolyType)
mty of
        Just (Embed PolyType -> Embedded (Embed PolyType)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty) -> Term -> PolyType -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Embedded (Embed Term)
Term
t Embedded (Embed PolyType)
PolyType
ty
        Maybe (Embed PolyType)
Nothing              -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
      (AGuard, TyCtx) -> Sem r (AGuard, TyCtx)
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( ABinding -> AGuard
AGLet (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> ABinding
ABinding Maybe (Embed PolyType)
mty (Name Term -> Name ATerm
coerce Name Term
x) (Embedded (Embed ATerm) -> Embed ATerm
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed ATerm)
ATerm
at))
        , QName Term -> PolyType -> TyCtx
forall a b. QName a -> b -> Ctx a b
singleCtx (Name Term -> QName Term
forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType (ATerm -> Type
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) = PolyType -> Sem r ()
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid PolyType
ty Sem r () -> Sem r ATerm -> Sem r ATerm
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> PolyType -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), 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 <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at) Type
ty
  ATerm -> Sem r ATerm
forall (m :: * -> *) a. Monad m => a -> m a
return (ATerm -> Sem r ATerm) -> ATerm -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Type -> ATerm -> ATerm
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 :: Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p (TyUser String
name [Type]
args) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args Sem r Type
-> (Type -> Sem r (TyCtx, APattern)) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p

checkPattern (PVar Name Term
x) Type
ty = (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName Term -> PolyType -> TyCtx
forall a b. QName a -> b -> Ctx a b
singleCtx (Name Term -> QName Term
forall a. Name a -> QName a
localName Name Term
x) (Type -> PolyType
toPolyType Type
ty), Type -> Name ATerm -> APattern
APVar Type
ty (Name Term -> Name ATerm
coerce Name Term
x))

checkPattern Pattern
PWild    Type
ty = (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
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...
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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.
  Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1

checkPattern Pattern
PUnit Type
ty = do
  Type -> Type -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyUnit
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
forall a b. Ctx a b
emptyCtx, APattern
APUnit)

checkPattern (PBool Bool
b) Type
ty = do
  Type -> Type -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyBool
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
forall a b. Ctx a b
emptyCtx, Bool -> APattern
APBool Bool
b)

checkPattern (PChar Char
c) Type
ty = do
  Type -> Type -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyC
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
forall a b. Ctx a b
emptyCtx, Char -> APattern
APChar Char
c)

checkPattern (PString String
s) Type
ty = do
  Type -> Type -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Type -> Type -> Sem r ()
ensureEq Type
ty Type
TyString
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
forall a b. Ctx a b
emptyCtx, String -> APattern
APString String
s)

checkPattern (PTup [Pattern]
tup) Type
tupTy = do
  [(TyCtx, APattern)]
listCtxtAps <- [Pattern] -> Type -> Sem r [(TyCtx, APattern)]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [Pattern]
tup Type
tupTy
  let ([TyCtx]
ctxs, [APattern]
aps) = [(TyCtx, APattern)] -> ([TyCtx], [APattern])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TyCtx, APattern)]
listCtxtAps
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCtx] -> TyCtx
forall a. Monoid a => [a] -> a
mconcat [TyCtx]
ctxs, Type -> [APattern] -> APattern
APTup ((Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Type -> Type -> Type
(:*:) ((APattern -> Type) -> [APattern] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Type
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 :: [Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [] Type
_   = String -> Sem r [(TyCtx, APattern)]
forall a. HasCallStack => String -> a
error String
"Impossible! checkTuplePat []"
    checkTuplePat [Pattern
p] Type
ty = do     -- (:[]) <$> check t ty
      (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
      [(TyCtx, APattern)] -> Sem r [(TyCtx, APattern)]
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) <- Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CProd Type
ty (Pattern -> Either Term Pattern
forall a b. b -> Either a b
Right (Pattern -> Either Term Pattern) -> Pattern -> Either Term Pattern
forall a b. (a -> b) -> a -> b
$ [Pattern] -> Pattern
PTup (Pattern
pPattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
:[Pattern]
ps))
      (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1
      [(TyCtx, APattern)]
rest <- [Pattern] -> Type -> Sem r [(TyCtx, APattern)]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [Pattern]
ps Type
ty2
      [(TyCtx, APattern)] -> Sem r [(TyCtx, APattern)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((TyCtx
ctx, APattern
apt) (TyCtx, APattern) -> [(TyCtx, APattern)] -> [(TyCtx, APattern)]
forall a. a -> [a] -> [a]
: [(TyCtx, APattern)]
rest)

checkPattern p :: Pattern
p@(PInj Side
L Pattern
pat) Type
ty       = do
  (Type
ty1, Type
ty2) <- Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CSum Type
ty (Pattern -> Either Term Pattern
forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty1
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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) <- Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
CSum Type
ty (Pattern -> Either Term Pattern
forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty2
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CSub Type
TyN Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
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 <- Con -> Type -> Either Term Pattern -> Sem r Type
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
CList Type
ty (Pattern -> Either Term Pattern
forall a b. b -> Either a b
Right Pattern
p)
  (TyCtx
ctx1, APattern
ap1) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p1 Type
tyl
  (TyCtx
ctx2, APattern
ap2) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p2 (Type -> Type
TyList Type
tyl)
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx1 TyCtx -> TyCtx -> TyCtx
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 <- Con -> Type -> Either Term Pattern -> Sem r Type
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), Writer Constraint, Error TCError,
    Fresh]
  r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
CList Type
ty (Pattern -> Either Term Pattern
forall a b. b -> Either a b
Right Pattern
p)
  [(TyCtx, APattern)]
listCtxtAps <- (Pattern -> Sem r (TyCtx, APattern))
-> [Pattern] -> Sem r [(TyCtx, APattern)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
`checkPattern` Type
tyl) [Pattern]
ps
  let ([TyCtx]
ctxs, [APattern]
aps) = [(TyCtx, APattern)] -> ([TyCtx], [APattern])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TyCtx, APattern)]
listCtxtAps
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCtx] -> TyCtx
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
  ATerm
at <- Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QSub Type
ty
  Type
tyInner <- Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
ty
  (TyCtx
ctx, APattern
apt) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
tyInner
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
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
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QDiv Type
ty
  Type
tyP <- Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
ty
  Type
tyQ <- Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
tyP
  (TyCtx
ctx1, APattern
ap1) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
tyP
  (TyCtx
ctx2, APattern
ap2) <- Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader (Map String TyDefBody), Writer Constraint,
    Error TCError, Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
q Type
tyQ
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCtx
ctx1 TyCtx -> TyCtx -> TyCtx
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 :: Type -> Type -> Sem r ()
cAbs Type
argTy Type
resTy = do
  Type
resTy' <- Type -> Sem r Type
forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cPos Type
argTy
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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 :: Type -> Type -> Sem r ()
cSize Type
argTy Type
resTy = do
  Type
a <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  Atom
c <- Sem r Atom
forall (r :: EffectRow). Member Fresh r => Sem r Atom
freshAtom
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Atom -> Type -> Type
TyContainer Atom
c Type
a) Type
argTy
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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 :: Type -> Sem r Type
cPos Type
ty = do
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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) -> Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
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).
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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
        ]
      Type -> Sem r Type
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 :: Type -> Sem r Type
cInt Type
ty = do
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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) -> Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Sem r Type) -> Type -> Sem r Type
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 <- Sem r Type
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).
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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
        ]
      Type -> Sem r Type
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 :: Type -> Type -> Sem r Type
cExp Type
ty1 Type
TyN = do
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Qualifier -> Type -> Constraint
CQual Qualifier
QNum Type
ty1
  Type -> Sem r Type
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 <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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.
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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]
    ]
  Type -> Sem r Type
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 :: Container -> Type -> Sem r Type
getEltTy Container
_ (TyContainer Atom
_ Type
e) = Type -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
e
getEltTy Container
c Type
ty = do
  Type
eltTy <- Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy
  Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Container -> Type -> Type
containerTy Container
c Type
eltTy) Type
ty
  Type -> Sem r Type
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 :: 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) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader (Map String TyDefBody), Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args Sem r Type -> (Type -> Sem r [Type]) -> Sem r [Type]
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
      [Type] -> Sem r [Type]
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 <- (Variance -> Sem r Type) -> [Variance] -> Sem r [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sem r Type -> Variance -> Sem r Type
forall a b. a -> b -> a
const Sem r Type
forall (r :: EffectRow). Member Fresh r => Sem r Type
freshTy) (Con -> [Variance]
arity Con
c1)
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
tyv (Con -> [Type] -> Type
TyCon Con
c1 [Type]
tyvs)
      [Type] -> Sem r [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
tyvs

    matchConTy Con
_ Type
_ = Sem r [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 Con -> Con -> Bool
forall a. Eq a => a -> a -> Bool
== Con
c2 = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    matchCon (CContainer v :: Atom
v@(AVar (U Name Type
_))) (CContainer Atom
ctr2) =
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
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
_))) =
      Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq (Atom -> Type
TyAtom Atom
ctr1) (Atom -> Type
TyAtom Atom
v)
    matchCon Con
_ Con
_                              = Sem r ()
forall a. Sem r a
matchError

    matchError :: Sem r a
    matchError :: Sem r a
matchError = case Either Term Pattern
targ of
      Left Term
term -> TCError -> Sem r a
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 -> TCError -> Sem r a
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 :: Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
c Type
ty Either Term Pattern
targ = do
  [Type]
tys <- Con -> Type -> Either Term Pattern -> Sem r [Type]
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), 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 -> Sem r Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty1
    [Type]
_     -> String -> Sem r Type
forall a. HasCallStack => String -> a
error (String -> Sem r Type) -> String -> Sem r Type
forall a b. (a -> b) -> a -> b
$
      String
"Impossible! Wrong number of arg types in ensureConstr1 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
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 :: Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
c Type
ty Either Term Pattern
targ  = do
  [Type]
tys <- Con -> Type -> Either Term Pattern -> Sem r [Type]
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), 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] -> (Type, Type) -> Sem r (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty1, Type
ty2)
    [Type]
_          -> String -> Sem r (Type, Type)
forall a. HasCallStack => String -> a
error (String -> Sem r (Type, Type)) -> String -> Sem r (Type, Type)
forall a b. (a -> b) -> a -> b
$
      String
"Impossible! Wrong number of arg types in ensureConstr2 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> String
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 :: Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
Infer      Either Term Pattern
_  = [Mode] -> Sem r [Mode]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Mode] -> Sem r [Mode]) -> [Mode] -> Sem r [Mode]
forall a b. (a -> b) -> a -> b
$ (Variance -> Mode) -> [Variance] -> [Mode]
forall a b. (a -> b) -> [a] -> [b]
map (Mode -> Variance -> Mode
forall a b. a -> b -> a
const Mode
Infer) (Con -> [Variance]
arity Con
c)
ensureConstrMode Con
c (Check Type
ty) Either Term Pattern
tp = (Type -> Mode) -> [Type] -> [Mode]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Mode
Check ([Type] -> [Mode]) -> Sem r [Type] -> Sem r [Mode]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Type -> Either Term Pattern -> Sem r [Type]
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), 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 :: Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- Con -> Mode -> Either Term Pattern -> Sem r [Mode]
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), 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 -> Sem r Mode
forall (m :: * -> *) a. Monad m => a -> m a
return Mode
m1
    [Mode]
_    -> String -> Sem r Mode
forall a. HasCallStack => String -> a
error (String -> Sem r Mode) -> String -> Sem r Mode
forall a b. (a -> b) -> a -> b
$
      String
"Impossible! Wrong number of arg types in ensureConstrMode1 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mode -> String
forall a. Show a => a -> String
show Mode
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Mode] -> String
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 :: Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- Con -> Mode -> Either Term Pattern -> Sem r [Mode]
forall (r :: EffectRow).
Members
  '[Reader (Map String TyDefBody), 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] -> (Mode, Mode) -> Sem r (Mode, Mode)
forall (m :: * -> *) a. Monad m => a -> m a
return (Mode
m1, Mode
m2)
    [Mode]
_        -> String -> Sem r (Mode, Mode)
forall a. HasCallStack => String -> a
error (String -> Sem r (Mode, Mode)) -> String -> Sem r (Mode, Mode)
forall a b. (a -> b) -> a -> b
$
      String
"Impossible! Wrong number of arg types in ensureConstrMode2 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mode -> String
forall a. Show a => a -> String
show Mode
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Mode] -> String
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 :: Type -> Type -> Sem r ()
ensureEq Type
ty1 Type
ty2
  | Type
ty1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty2 = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise  = Constraint -> Sem r ()
forall (r :: EffectRow).
Member (Writer Constraint) r =>
Constraint -> Sem r ()
constraint (Constraint -> Sem r ()) -> Constraint -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEq Type
ty1 Type
ty2