{-# 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 (filterM, forM_, replicateM, unless, when, zipWithM)
import Control.Monad.Trans.Maybe
import Data.Bifunctor (first)
import Data.Coerce
import qualified Data.Foldable as F
import Data.List (sort)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
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 Disco.AST.Surface
import Disco.AST.Typed
import Disco.Context hiding (filter)
import qualified Disco.Context as Ctx
import Disco.Effects.Fresh
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.Solve (SolutionLimit (..), solveConstraint)
import Disco.Typecheck.Util
import Disco.Types
import Disco.Types.Rules
import Polysemy hiding (embed)
import Polysemy.Error
import Polysemy.Input
import Polysemy.Output
import Polysemy.Reader
import Polysemy.State (evalState)
import Polysemy.Writer
import Text.EditDistance (defaultEditCosts, restrictedDamerauLevenshteinDistance)
import Unbound.Generics.LocallyNameless (
  Alpha,
  Bind,
  Name,
  bind,
  embed,
  name2String,
  string2Name,
  substs,
  unembed,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
import Prelude as P hiding (lookup)

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

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

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

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

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

------------------------------------------------------------
-- Variable name utilities
------------------------------------------------------------

suggestionsFrom :: String -> [String] -> [String]
suggestionsFrom :: String -> [String] -> [String]
suggestionsFrom String
x = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) (Int -> Bool) -> (String -> Int) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EditCosts -> String -> String -> Int
restrictedDamerauLevenshteinDistance EditCosts
defaultEditCosts String
x)

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

-- | Check all the types and extract all relevant info (docs,
--   properties, types) from a module, returning a 'ModuleInfo' record
--   on success.  This function does not handle imports at all; any
--   imports should already be checked and passed in as the second
--   argument.
checkModule ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r =>
  ModuleName ->
  Map ModuleName ModuleInfo ->
  Module ->
  Sem r ModuleInfo
checkModule :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error LocTCError, Fresh]
  r =>
ModuleName
-> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo
checkModule ModuleName
name Map ModuleName ModuleInfo
imports (Module Set Ext
es [String]
_ [Decl]
m [(Name Term, Docs)]
docs [Term]
terms) = do
  let ([TypeDecl]
typeDecls, [TermDefn]
defns, [TypeDefn]
tydefs) = [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
m
      importTyCtx :: TyCtx
importTyCtx = [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map ModuleName a -> f (Map ModuleName 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 :: TyDefCtx
importTyDefnCtx = [TyDefCtx] -> TyDefCtx
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 [TyDefCtx]) (Map ModuleName ModuleInfo) TyDefCtx
-> [TyDefCtx]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map ModuleName a -> f (Map ModuleName b)
traverse ((ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo))
-> ((TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
    -> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> Getting (Endo [TyDefCtx]) (Map ModuleName ModuleInfo) TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
-> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs)
  TyDefCtx
tyDefnCtx <- (TCError -> LocTCError)
-> Sem (Error TCError : r) TyDefCtx -> Sem r TyDefCtx
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) TyDefCtx -> Sem r TyDefCtx)
-> Sem (Error TCError : r) TyDefCtx -> Sem r TyDefCtx
forall a b. (a -> b) -> a -> b
$ [TypeDefn] -> Sem (Error TCError : r) TyDefCtx
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
[TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx [TypeDefn]
tydefs
  TyDefCtx -> Sem r ModuleInfo -> Sem r ModuleInfo
forall (r :: EffectRow) a.
Member (Reader TyDefCtx) r =>
TyDefCtx -> Sem r a -> Sem r a
withTyDefns (TyDefCtx
tyDefnCtx TyDefCtx -> TyDefCtx -> TyDefCtx
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TyDefCtx
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 TyDefCtx, 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 TyDefCtx, 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ModuleName -> TermDefn -> Sem r Defn
forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh,
    Output (Message ann)]
  r =>
ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name) [TermDefn]
defns
      let defnCtx :: Ctx ATerm Defn
defnCtx = 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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
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
forall a b. Coercible a b => a -> b
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 ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docCtx -- XXX location?
          [(ATerm, PolyType)]
aterms <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term -> Sem (Error TCError : r) (ATerm, PolyType)
forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 [Term]
terms -- XXX location?
          ModuleInfo -> Sem r ModuleInfo
forall a. a -> Sem r a
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
-> TyDefCtx
-> 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 TyDefCtx
tyDefnCtx Ctx ATerm Defn
defnCtx [(ATerm, PolyType)]
aterms Set Ext
es
 where
  getDefnName :: Defn -> Name ATerm
  getDefnName :: Defn -> Name ATerm
getDefnName (Defn Name ATerm
n [Type]
_ Type
_ NonEmpty Clause
_) = Name ATerm
n

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

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

-- | Turn a list of type definitions into a 'TyDefCtx', checking
--   for duplicate names among the definitions and also any type
--   definitions already in the context.
makeTyDefnCtx :: Members '[Reader TyDefCtx, Error TCError] r => [TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
[TypeDefn] -> Sem r TyDefCtx
makeTyDefnCtx [TypeDefn]
tydefs = do
  TyDefCtx
oldTyDefs <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  let oldNames :: [String]
oldNames = TyDefCtx -> [String]
forall k a. Map k a -> [k]
M.keys TyDefCtx
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 TyDefCtx
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> TCError
DuplicateTyDefns String
x)
    [] -> TyDefCtx -> Sem r TyDefCtx
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyDefCtx -> Sem r TyDefCtx)
-> ([(String, TyDefBody)] -> TyDefCtx)
-> [(String, TyDefBody)]
-> Sem r TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, TyDefBody)] -> TyDefCtx
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, TyDefBody)] -> Sem r TyDefCtx)
-> [(String, TyDefBody)] -> Sem r TyDefCtx
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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error LocTCError] r =>
ModuleName -> TypeDefn -> Sem r ()
checkTyDefn ModuleName
name defn :: TypeDefn
defn@(TypeDefn String
x [String]
args Type
body) = (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 TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
body

  -- Now make sure it is not directly cyclic (i.e. ensure it is a
  -- "productive" definition).
  Set String
_ <- Type -> Set String -> Sem (Error TCError : r) (Set String)
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy (String -> [Type] -> Type
TyUser String
x ((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 TyDefCtx, Error TCError] r =>
TypeDefn -> Sem r ()
checkUnboundVars TypeDefn
defn

  -- Make sure it does not use any polymorphic recursion (polymorphic
  -- recursion isn't allowed at the moment since it can make the
  -- subtyping checker diverge).
  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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Set String -> Sem r (Set String)
checkCyclicTy (TyUser String
name [Type]
args) Set String
set = do
  case 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 TyDefCtx, 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 TyDefCtx, 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Set String
set

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

-- | Keep only the duplicate elements from a list.
--
--   >>> filterDups [1,3,2,1,1,4,2]
--   [1,2]
filterDups :: Ord a => [a] -> [a]
filterDups :: forall a. Ord a => [a] -> [a]
filterDups = (NonEmpty a -> a) -> [NonEmpty a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty a -> a
forall a. NonEmpty a -> a
NE.head ([NonEmpty a] -> [a]) -> ([a] -> [NonEmpty a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty a -> Bool) -> [NonEmpty a] -> [NonEmpty a]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Int -> Bool) -> (NonEmpty a -> Int) -> NonEmpty a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> Int
forall a. NonEmpty a -> Int
NE.length) ([NonEmpty a] -> [NonEmpty a])
-> ([a] -> [NonEmpty a]) -> [a] -> [NonEmpty a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [NonEmpty a]
forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
NE.group ([a] -> [NonEmpty a]) -> ([a] -> [a]) -> [a] -> [NonEmpty 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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
ModuleName -> [TypeDecl] -> Sem r TyCtx
makeTyCtx ModuleName
name [TypeDecl]
decls = do
  let dups :: [Name Term]
dups = [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 TyDefCtx, Error TCError] r =>
TyCtx -> Sem r ()
checkCtx TyCtx
declCtx
      TyCtx -> Sem r TyCtx
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
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 TyDefCtx, 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 ann)] r =>
  ModuleName ->
  TermDefn ->
  Sem r Defn
checkDefn :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh,
    Output (Message ann)]
  r =>
ModuleName -> TermDefn -> Sem r Defn
checkDefn ModuleName
name (TermDefn Name Term
x NonEmpty (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
  Sem (Error TCError : r) (Doc ann) -> Sem (Error TCError : r) ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem (Error TCError : r) (Doc ann)
"======================================================================"
  Sem (Error TCError : r) (Doc ann) -> Sem (Error TCError : r) ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem (Error TCError : r) (Doc ann)
"Checking definition:"
  -- Check that all clauses have the same number of patterns
  NonEmpty (Bind [Pattern] Term) -> Sem (Error TCError : r) ()
checkNumPats NonEmpty (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 a b.
Sem (Error TCError : r) a
-> (a -> Sem (Error TCError : r) b) -> Sem (Error TCError : r) b
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 a. a -> Sem (Error TCError : r) a
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 TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Bind [Pattern] Term -> Int
numPats (NonEmpty (Bind [Pattern] Term) -> Bind [Pattern] Term
forall a. NonEmpty a -> a
NE.head NonEmpty (Bind [Pattern] Term)
clauses)) Type
ty

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

  Defn -> Sem (Error TCError : r) Defn
forall a. a -> Sem (Error TCError : r) a
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 (NonEmpty S -> S
forall a. NonEmpty a -> a
NE.head NonEmpty S
thetas) (Name ATerm -> [Type] -> Type -> NonEmpty Clause -> Defn
Defn (Name Term -> Name ATerm
forall a b. Coercible a b => a -> b
coerce Name Term
x) [Type]
patTys Type
bodyTy NonEmpty Clause
acs)
 where
  numPats :: Bind [Pattern] Term -> Int
numPats = [Pattern] -> Int
forall a. [a] -> 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 :: NonEmpty (Bind [Pattern] Term) -> Sem (Error TCError : r) ()
checkNumPats (Bind [Pattern] Term
_ :| []) = () -> Sem (Error TCError : r) ()
forall a. a -> Sem (Error TCError : r) a
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
c Bind [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 a. a -> Sem (Error TCError : r) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- Check a clause of a definition against a list of pattern types and a body type.
  checkClause ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    [Type] ->
    Type ->
    Bind [Pattern] Term ->
    Sem r Clause
  checkClause :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Type] -> Type -> Bind [Pattern] Term -> Sem r Clause
checkClause [Type]
patTys Type
bodyTy Bind [Pattern] Term
clause = do
    ([Pattern]
pats, Term
body) <- 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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
body Type
bodyTy
    Clause -> Sem r Clause
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
0 Type
ty = ([Type], Type) -> Sem r ([Type], Type)
forall a. a -> Sem r a
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 TyDefCtx, 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 a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Type -> Sem r ([Type], Type)
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy Int
n
  decomposeDefnTy Int
n (Type
ty1 :->: Type
ty2) = ([Type] -> [Type]) -> ([Type], Type) -> ([Type], Type)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type
ty1 Type -> [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 TyDefCtx, Error TCError] r =>
Int -> Type -> Sem r ([Type], Type)
decomposeDefnTy (Int
n Int -> 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 ann)] r =>
  Ctx Term Docs ->
  Sem r (Ctx ATerm [AProperty])
checkProperties :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Ctx Term Docs -> Sem r (Ctx ATerm [ATerm])
checkProperties Ctx Term Docs
docs =
  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 a. [a] -> 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ctx Term a -> f (Ctx Term 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) Term -> Sem r ATerm
forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Term -> Sem r ATerm
checkProperty Ctx Term [Term]
properties
 where
  properties :: Ctx Term [Property]
  properties :: Ctx Term [Term]
properties = (Docs -> [Term]) -> Ctx Term Docs -> Ctx Term [Term]
forall a b. (a -> b) -> Ctx Term a -> Ctx Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Docs
ds -> [Term
p | DocProperty Term
p <- Docs
ds]) Ctx Term Docs
docs

-- | Check the types of the terms embedded in a property.
checkProperty ::
  Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r =>
  Property ->
  Sem r AProperty
checkProperty :: forall ann (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output (Message ann)]
  r =>
Term -> Sem r ATerm
checkProperty Term
prop = do
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"======================================================================"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking property:"
  Term -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Term
prop
  (ATerm
at, NonEmpty S
thetas) <- Int
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Int -> Sem (Writer Constraint : r) a -> Sem r (a, NonEmpty S)
solve Int
1 (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
prop Type
TyProp
  -- XXX do we need to default container variables here?
  ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 (NonEmpty S -> S
forall a. NonEmpty a -> a
NE.head NonEmpty S
thetas) ATerm
at

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

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

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

-- | Disco doesn't need kinds per se, since all types must be fully
--   applied.  But we do need to check that every type is applied to
--   the correct number of arguments.
checkTypeValid :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Sem r ()
checkTypeValid :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid (TyAtom Atom
_) = () -> Sem r ()
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid [Type]
tys
 where
  n :: Int
n = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys

conArity :: Members '[Reader TyDefCtx, Error TCError] r => Con -> Sem r Int
conArity :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Con -> Sem r Int
conArity (CContainer Atom
_) = Int -> Sem r Int
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity Con
CGraph = Int -> Sem r Int
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
1
conArity (CUser String
name) = do
  TyDefCtx
d <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyDefCtx
  case String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name TyDefCtx
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
as)
conArity Con
_ = Int -> Sem r Int
forall a. a -> Sem r a
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
$cshowsPrec :: Int -> Mode -> ShowS
showsPrec :: Int -> Mode -> ShowS
$cshow :: Mode -> String
show :: Mode -> String
$cshowList :: [Mode] -> ShowS
showList :: [Mode] -> ShowS
Show)

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

-- | Check that a term has the given polymorphic type.
checkPolyTy ::
  Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Term ->
  PolyType ->
  Sem r ATerm
checkPolyTy :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t (Forall Bind [Name Type] Type
sig) = do
  ([Name Type]
as, Type
tau) <- 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 TyDefCtx, 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ATerm
at

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

-- | Top-level type inference algorithm, returning only the first
--   possible result.
inferTop1 ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
  Term ->
  Sem r (ATerm, PolyType)
inferTop1 :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 Term
t = NonEmpty (ATerm, PolyType) -> (ATerm, PolyType)
forall a. NonEmpty a -> a
NE.head (NonEmpty (ATerm, PolyType) -> (ATerm, PolyType))
-> Sem r (NonEmpty (ATerm, PolyType)) -> Sem r (ATerm, PolyType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Term -> Sem r (NonEmpty (ATerm, PolyType))
forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Int -> Term -> Sem r (NonEmpty (ATerm, PolyType))
inferTop Int
1 Term
t

-- | Top-level type inference algorithm: infer up to the requested max
--   number of possible (polymorphic) types for a term by running type
--   inference, solving the resulting constraints, and quantifying
--   over any remaining type variables.
inferTop ::
  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
  Int ->
  Term ->
  Sem r (NonEmpty (ATerm, PolyType))
inferTop :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Int -> Term -> Sem r (NonEmpty (ATerm, PolyType))
inferTop Int
lim Term
t = do
  -- Run inference on the term and try to solve the resulting
  -- constraints.
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"======================================================================"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Inferring the type of:"
  Term -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Term
t
  (ATerm
at, NonEmpty S
thetas) <- Int
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Int -> Sem (Writer Constraint : r) a -> Sem r (a, NonEmpty S)
solve Int
lim (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall a b. (a -> b) -> a -> b
$ Term -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t

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

  -- Currently the following code generates *every possible*
  -- combination of substitutions for container variables, which can
  -- lead to exponential blowup in some cases.  For example, inferring
  -- the type of
  --
  --   \x. \y. \z. (set(x), set(y), set(z))
  --
  -- takes a Very Long Time.  Potential solutions include:
  --
  --   1. Do something similar as in the 'solve' function, using a State SolutionLimit
  --      effect to stop early once we've generated enough variety.
  --
  --   2. Use a proper backtracking search monad like LogicT to scope
  --      over both the generation of solution substitutions *and*
  --      choosing container variable monomorphizations, then just
  --      take a limited number of solutions.  Unfortunately,
  --      polysemy's NonDet effect seems to be somewhat broken
  --      (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy
  --      ; https://github.com/polysemy-research/polysemy/issues/246 )
  --      and using LogicT on top of Sem is going to be tedious since
  --      it would require calling 'lift' on almost everything.
  --
  --   3. Also, it is probably (?) the case that no matter which of
  --      the generated substitutions is used, the exact same
  --      container variables are still unconstrained in all of them.
  --      So we should be able to pick container variable
  --      monomorphizations independently of the substitutions from
  --      the solver.  Doing this would help though it would not
  --      address the fundamental issue.

  -- Quantify over any remaining type variables and return
  -- the term along with the resulting polymorphic type.
  NonEmpty (ATerm, PolyType) -> Sem r (NonEmpty (ATerm, PolyType))
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (ATerm, PolyType) -> Sem r (NonEmpty (ATerm, PolyType)))
-> NonEmpty (ATerm, PolyType) -> Sem r (NonEmpty (ATerm, PolyType))
forall a b. (a -> b) -> a -> b
$ do
    -- Monad NonEmpty

    -- Iterate over all possible solutions...
    S
theta <- NonEmpty S
thetas

    let -- Apply each one...
        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')

    -- Build all possible substitutions for those container variables...
    [Type]
ctrs <- Int -> NonEmpty Type -> NonEmpty [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Set (Name Type) -> Int
forall a. Set a -> Int
S.size Set (Name Type)
cvs) ((BaseTy -> Type) -> NonEmpty BaseTy -> NonEmpty Type
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (Atom -> Type
TyAtom (Atom -> Type) -> (BaseTy -> Atom) -> BaseTy -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseTy -> Atom
ABase) (BaseTy
CtrList BaseTy -> [BaseTy] -> NonEmpty BaseTy
forall a. a -> [a] -> NonEmpty a
:| [BaseTy
CtrBag, BaseTy
CtrSet]))

    -- Substitute for the container variables...
    let 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]
ctrs) ATerm
at'

    -- Return the term along with its type, with all substitutions applied.
    (ATerm, PolyType) -> NonEmpty (ATerm, PolyType)
forall a. a -> NonEmpty a
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 ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
  Term ->
  PolyType ->
  Sem r ATerm
checkTop :: forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkTop Term
t PolyType
ty = do
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"======================================================================"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking the type of:"
  Term -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty Term
t
  PolyType -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty PolyType
ty
  (ATerm
at, NonEmpty S
theta) <- Int
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall ann (r :: EffectRow) a.
Members
  '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
Int -> Sem (Writer Constraint : r) a -> Sem r (a, NonEmpty S)
solve Int
1 (Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S))
-> Sem (Writer Constraint : r) ATerm -> Sem r (ATerm, NonEmpty S)
forall a b. (a -> b) -> a -> b
$ Term -> PolyType -> Sem (Writer Constraint : r) ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t PolyType
ty
  ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 (NonEmpty S -> S
forall a. NonEmpty a -> a
NE.head NonEmpty S
theta) ATerm
at

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

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

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

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

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

-- Resolve variable names and infer their types.  We don't need a
-- checking case; checking the type of a variable will fall through to
-- this case.
typecheck Mode
Infer (TVar Name Term
x) = do
  -- Pick the first method that succeeds; if none do, throw an unbound
  -- variable error.
  Maybe ATerm
mt <- 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]
  TyCtx
ctx <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @TyCtx
  let inScope :: [String]
inScope = (Name Term -> String) -> [Name Term] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name Term -> String
forall a. Name a -> String
name2String (TyCtx -> [Name Term]
forall a b. Ctx a b -> [Name a]
Ctx.names TyCtx
ctx) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
opNames [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
syn | PrimInfo Prim
_ String
syn Bool
_ <- Map Prim PrimInfo -> [PrimInfo]
forall k a. Map k a -> [a]
M.elems Map Prim PrimInfo
primMap]
      suggestions :: [String]
suggestions = String -> [String] -> [String]
suggestionsFrom (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) [String]
inScope
  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 (TCError -> Sem r ATerm) -> TCError -> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Name Term -> [String] -> TCError
Unbound Name Term
x [String]
suggestions) ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
coerce Name Term
x))
      Maybe PolyType
Nothing -> Maybe ATerm -> Sem r (Maybe ATerm)
forall a. a -> Sem r a
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 a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
coerce Name Term
x)
      [] -> Maybe ATerm -> Sem r (Maybe ATerm)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ATerm
forall a. Maybe a
Nothing
      [(ModuleName, PolyType)]
_nonEmpty -> 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
Infer (Prim -> Term
TPrim Prim
prim)
      [] -> Maybe ATerm -> Sem r (Maybe ATerm)
forall a. a -> Sem r a
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 a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
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 a. a -> Sem r a
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 a. a -> Sem r a
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

  inferPrim (PrimBOp BOp
op) | BOp
op BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
And, BOp
Or, BOp
Impl, BOp
Iff] = 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 a. a -> Sem r a
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
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
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
QBool Type
a
    Type -> Sem r Type
forall a. a -> Sem r a
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

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

  inferPrim Prim
conv | Prim
conv Prim -> [Prim] -> Bool
forall a. Eq a => a -> [a] -> 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> 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 a. a -> Sem r a
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 a. a -> Sem r a
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

  ----------------------------------------
  -- Randomness

  inferPrim Prim
PrimRandom = Type -> Sem r Type
forall a. a -> Sem r a
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
TyGen Type -> Type -> Type
:->: (Type
TyN Type -> Type -> Type
:*: Type
TyGen)
  inferPrim Prim
PrimSeed = Type -> Sem r Type
forall a. a -> Sem r a
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
TyGen
  ----------------------------------------
  -- 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 binary assertion is just like a comparison, except
  -- the result is a Prop.
  inferPrim (PrimBOp (Should BOp
_)) = 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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> 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 a. a -> Sem r a
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"
  ------------------------------------------------------------

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

  inferPrim (PrimUOp UOp
Fact) = Type -> Sem r Type
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> 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 a. a -> Sem r a
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 ()
`orElse` 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 a. a -> Sem r a
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

  ----------------------------------------
  -- min/max

  inferPrim Prim
PrimMin = 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
QCmp Type
a
    Type -> Sem r Type
forall a. a -> Sem r a
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 Prim
PrimMax = 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
QCmp Type
a
    Type -> Sem r Type
forall a. a -> Sem r a
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

  ----------------------------------------
  -- 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ATerm
ATUnit
typecheck Mode
Infer (TBool Bool
b) = ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [Pattern]
args Type
checkTy Term
tm

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

  -- If we're all out of arguments, the remaining checking type is the
  -- result, and there are no variables to bind in the context.
  checkArgs :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Term -> Sem r (TyCtx, [APattern], Type)
checkArgs [] Type
ty Term
_ = (TyCtx, [APattern], Type) -> Sem r (TyCtx, [APattern], Type)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty1

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

    -- Pass the result type through, and put the pattern-bound variables
    -- in the returned context.
    (TyCtx, [APattern], Type) -> Sem r (TyCtx, [APattern], Type)
forall a. a -> Sem r a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Pattern -> Sem r Type
forall (r :: EffectRow).
Members '[Reader TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern [Pattern]
args [Type]
tys

  -- In the case of ∀, ∃, have to ensure that the argument types are
  -- searchable.
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Quantifier
q Quantifier -> [Quantifier] -> Bool
forall a. Eq a => a -> [a] -> 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t
        ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
TyProp
        ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError, Fresh] r =>
Pattern -> Sem r Type
getAscrOrFresh (PAscr Pattern
_ Type
ty) = Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
ty Sem r () -> Sem r Type -> Sem r Type
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> Sem r Type
forall a. a -> Sem r a
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 a b. (a -> b -> b) -> b -> [a] -> b
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 TyDefCtx, 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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t' Type
ty1

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

-- Check/infer the type of a tuple.
typecheck Mode
mode1 (TTup [Term]
tup) = (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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
mode1 [Term]
tup
 where
  typecheckTuple ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Mode ->
    [Term] ->
    Sem r (Type, [ATerm])
  typecheckTuple :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
_ [] = 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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t
  typecheckTuple Mode
mode (Term
t : [Term]
ts) = do
    (Mode
m, Mode
ms) <- Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
CProd Mode
mode (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
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ts))
    ATerm
at <- Mode -> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
m Term
t
    (Type
ty, [ATerm]
ats) <- Mode -> [Term] -> Sem r (Type, [ATerm])
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> [Term] -> Sem r (Type, [ATerm])
typecheckTuple Mode
ms [Term]
ts
    (Type, [ATerm]) -> Sem r (Type, [ATerm])
forall a. a -> Sem r a
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_ UD]
ls) =
  Type -> ATerm -> [Link_ TY] -> ATerm
ATChain Type
TyBool (ATerm -> [Link_ TY] -> ATerm)
-> Sem r ATerm -> Sem r ([Link_ TY] -> ATerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Term
t Sem r ([Link_ TY] -> ATerm) -> Sem r [Link_ TY] -> Sem r ATerm
forall a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> [Link_ UD] -> Sem r [Link_ TY]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
t [Link_ UD]
ls
 where
  inferChain ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Term ->
    [Link] ->
    Sem r [ALink]
  inferChain :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
_ [] = [Link_ TY] -> Sem r [Link_ TY]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  inferChain Term
t1 (TLink BOp
op Term
t2 : [Link_ UD]
links) = do
    ATerm
at2 <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check (BOp -> Term -> Term -> Term
TBin BOp
op Term
t1 Term
t2) Type
TyBool
    [Link_ TY]
atl <- Term -> [Link_ UD] -> Sem r [Link_ TY]
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> [Link_ UD] -> Sem r [Link_ TY]
inferChain Term
t2 [Link_ UD]
links
    [Link_ TY] -> Sem r [Link_ TY]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Link_ TY] -> Sem r [Link_ TY]) -> [Link_ TY] -> Sem r [Link_ TY]
forall a b. (a -> b) -> a -> b
$ BOp -> ATerm -> Link_ TY
ATLink BOp
op ATerm
at2 Link_ TY -> [Link_ TY] -> [Link_ TY]
forall a. a -> [a] -> [a]
: [Link_ TY]
atl

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

typecheck Mode
Infer (TTyOp TyOp
Enumerate Type
t) = do
  Type -> Sem r ()
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 TyDefCtx, Error TCError] r =>
Type -> Sem r ()
checkTypeValid Type
t
  ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 TyDefCtx, 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 TyDefCtx, 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 a b. Sem r (a -> b) -> Sem r a -> Sem r b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Term -> Type -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
`check` Type
TyN) Maybe Term
n) [(Term, Maybe Term)]
xs
  Maybe (Ellipsis ATerm)
aell <- Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
typecheckEllipsis Mode
eltMode Maybe (Ellipsis Term)
ell
  Type
resTy <- case Mode
mode of
    Mode
Infer -> do
      let tys :: [Type]
tys = [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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. [a] -> 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 a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Maybe (Ellipsis Term) -> Sem r (Maybe (Ellipsis ATerm))
typecheckEllipsis Mode
_ Maybe (Ellipsis Term)
Nothing = Maybe (Ellipsis ATerm) -> Sem r (Maybe (Ellipsis ATerm))
forall a. a -> Sem r a
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
m Term
tm

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

-- Container comprehensions
typecheck Mode
mode tcc :: Term
tcc@(TContainerComp Container
c Bind (Telescope (Qual_ UD)) Term
bqt) = do
  Mode
eltMode <- Con -> Mode -> Either Term Pattern -> Sem r Mode
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 (Container -> Con
containerToCon Container
c) Mode
mode (Term -> Either Term Pattern
forall a b. a -> Either a b
Left Term
tcc)
  (Telescope (Qual_ UD)
qs, Term
t) <- Bind (Telescope (Qual_ UD)) Term
-> Sem r (Telescope (Qual_ UD), Term)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Qual_ UD)) Term
bqt
  (Telescope (Qual_ TY)
aqs, TyCtx
cx) <- (Qual_ UD -> Sem r (Qual_ TY, TyCtx))
-> Telescope (Qual_ UD) -> Sem r (Telescope (Qual_ TY), 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_ UD -> Sem r (Qual_ TY, TyCtx)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Qual_ UD -> Sem r (Qual_ TY, TyCtx)
inferQual Telescope (Qual_ UD)
qs
  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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
eltMode Term
t
    let resTy :: Type
resTy = case Mode
mode of
          Mode
Infer -> Container -> Type -> Type
containerTy Container
c (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at)
          Check Type
ty -> Type
ty
    ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 (Qual_ TY)) ATerm -> ATerm
ATContainerComp Type
resTy Container
c (Telescope (Qual_ TY) -> ATerm -> Bind (Telescope (Qual_ TY)) ATerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Qual_ TY)
aqs ATerm
at)
 where
  inferQual ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Qual ->
    Sem r (AQual, TyCtx)
  inferQual :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Qual_ UD -> Sem r (Qual_ TY, TyCtx)
inferQual (QBind Name Term
x (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 TyDefCtx, 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 TyDefCtx, 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)
    (Qual_ TY, TyCtx) -> Sem r (Qual_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ATerm -> Embed ATerm -> Qual_ TY
AQBind (Name Term -> Name ATerm
forall a b. Coercible a b => a -> b
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
Term
t Type
TyBool
    (Qual_ TY, TyCtx) -> Sem r (Qual_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> Qual_ TY
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_ UD)) Term
l) = do
  (Telescope (Binding_ UD)
bs, Term
t2) <- Bind (Telescope (Binding_ UD)) Term
-> Sem r (Telescope (Binding_ UD), Term)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Telescope (Binding_ UD)) Term
l

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

  -- ...then check/infer the body under an extended context.
  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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t2
    ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 (Binding_ TY)) ATerm -> ATerm
ATLet (ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at2) (Telescope (Binding_ TY)
-> ATerm -> Bind (Telescope (Binding_ TY)) ATerm
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Binding_ TY)
as ATerm
at2)
 where
  -- Infer the type of a binding (@x [: ty] = t@), returning a
  -- type-annotated binding along with a (singleton) context for the
  -- bound variable.  The optional type annotation on the variable
  -- determines whether we use inference or checking mode for the
  -- body.
  inferBinding ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Binding ->
    Sem r (ABinding, TyCtx)
  inferBinding :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Binding_ UD -> Sem r (Binding_ TY, TyCtx)
inferBinding (Binding Maybe (Embed PolyType)
mty Name Term
x (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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
    (Binding_ TY, TyCtx) -> Sem r (Binding_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> Binding_ TY
ABinding Maybe (Embed PolyType)
mty (Name Term -> Name ATerm
forall a b. Coercible a b => a -> b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Branch -> Sem r ABranch
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Branch -> Sem r ABranch
typecheckBranch [Branch]
bs
  Type
resTy <- case Mode
mode of
    Check Type
ty -> Type -> Sem r Type
forall a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
x
  ATerm -> Sem r ATerm
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Branch -> Sem r ABranch
typecheckBranch Branch
b = do
    (Telescope (Guard_ UD)
gs, Term
t) <- 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 (Guard_ TY)
ags, TyCtx
ctx) <- (Guard_ UD -> Sem r (Guard_ TY, TyCtx))
-> Telescope (Guard_ UD) -> Sem r (Telescope (Guard_ TY), 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 (Guard_ TY, TyCtx)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Guard_ UD -> Sem r (Guard_ TY, TyCtx)
inferGuard Telescope (Guard_ UD)
gs
    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 (Guard_ TY) -> ATerm -> ABranch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope (Guard_ TY)
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Mode -> Term -> Sem r ATerm
typecheck Mode
mode Term
t

  -- Infer the type of a guard, returning the type-annotated guard
  -- along with a context of types for any variables bound by the
  -- guard.
  inferGuard ::
    Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
    Guard ->
    Sem r (AGuard, TyCtx)
  inferGuard :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Guard_ UD -> Sem r (Guard_ TY, TyCtx)
inferGuard (GBool (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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Embedded (Embed Term)
Term
t Type
TyBool
    (Guard_ TY, TyCtx) -> Sem r (Guard_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> Guard_ TY
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 TyDefCtx, 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 TyDefCtx, 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)
    (Guard_ TY, TyCtx) -> Sem r (Guard_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed ATerm -> APattern -> Guard_ TY
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Sem r ATerm
infer Embedded (Embed Term)
Term
t
    (Guard_ TY, TyCtx) -> Sem r (Guard_ TY, TyCtx)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return
      ( Binding_ TY -> Guard_ TY
AGLet (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> Binding_ TY
ABinding Maybe (Embed PolyType)
mty (Name Term -> Name ATerm
forall a b. Coercible a b => a -> b
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 TyDefCtx, Error TCError] r =>
PolyType -> Sem r ()
checkPolyTyValid PolyType
ty Sem r () -> Sem r ATerm -> Sem r ATerm
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> PolyType -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkPolyTy Term
t PolyType
ty
--------------------------------------------------
-- Inference fallback

-- Finally, to check anything else, we can fall back to inferring its
-- type and then check that the inferred type is a *subtype* of the
-- given type.  We have to be careful to call 'setType' to change the
-- type at the root of the term to the requested type.
typecheck (Check Type
ty) Term
t = do
  ATerm
at <- Term -> Sem r ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, 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 a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern (PNonlinear Pattern
p Name Term
x) Type
_ = TCError -> Sem r (TyCtx, APattern)
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (TCError -> Sem r (TyCtx, APattern))
-> TCError -> Sem r (TyCtx, APattern)
forall a b. (a -> b) -> a -> b
$ Pattern -> Name Term -> TCError
NonlinearPattern Pattern
p Name Term
x
checkPattern Pattern
p (TyUser String
name [Type]
args) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader TyDefCtx, 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 a b. Sem r a -> (a -> Sem r b) -> Sem r b
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 TyDefCtx, 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 a. a -> Sem r a
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
forall a b. Coercible a b => a -> b
coerce Name Term
x))
checkPattern Pattern
PWild Type
ty = (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 a. a -> Sem r a
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 TyDefCtx, 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 a. a -> Sem r a
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 a. (a -> a -> a) -> [a] -> a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
ty
    [(TyCtx, APattern)] -> Sem r [(TyCtx, APattern)]
forall a. a -> Sem r a
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 TyDefCtx, 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
p Pattern -> [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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
[Pattern] -> Type -> Sem r [(TyCtx, APattern)]
checkTuplePat [Pattern]
ps Type
ty2
    [(TyCtx, APattern)] -> Sem r [(TyCtx, APattern)]
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty1
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
pat Type
ty2
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, 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 TyDefCtx, 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 a. a -> Sem r a
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 TyDefCtx, 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Pattern -> Type -> Sem r (TyCtx, APattern)
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
`checkPattern` Type
tyl) [Pattern]
ps
  let ([TyCtx]
ctxs, [APattern]
aps) = [(TyCtx, APattern)] -> ([TyCtx], [APattern])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TyCtx, APattern)]
listCtxtAps
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Term -> Type -> Sem r ATerm
check Term
t Type
ty
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
p Type
tyInner
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 TyDefCtx, 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 TyDefCtx, Writer Constraint, Error TCError,
    Fresh]
  r =>
Pattern -> Type -> Sem r (TyCtx, APattern)
checkPattern Pattern
q Type
tyQ
  (TyCtx, APattern) -> Sem r (TyCtx, APattern)
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
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 :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
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 :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
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 a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
res
 where
  pos :: BaseTy -> BaseTy
pos BaseTy
Z = BaseTy
N
  pos BaseTy
Q = BaseTy
F
  pos BaseTy
t = BaseTy
t

-- | Given an input type @ty@, return a type which represents the
--   output type of the floor or ceiling functions, and generate
--   appropriate constraints.
cInt :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type
cInt :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Sem r Type
cInt Type
ty = do
  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 a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
res
 where
  int :: BaseTy -> BaseTy
int BaseTy
F = BaseTy
N
  int BaseTy
Q = BaseTy
Z
  int BaseTy
t = BaseTy
t

-- | Given input types to the exponentiation operator, return a type
--   which represents the output type, and generate appropriate
--   constraints.
cExp :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r Type
cExp :: forall (r :: EffectRow).
Members '[Writer Constraint, Fresh] r =>
Type -> Type -> Sem r Type
cExp Type
ty1 Type
TyN = do
  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 a. a -> Sem r a
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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
resTy

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

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

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

  -- expand type definitions lazily
  matchConTy :: Con -> Type -> Sem r [Type]
matchConTy Con
c1 (TyUser String
name [Type]
args) = String -> [Type] -> Sem r Type
forall (r :: EffectRow).
Members '[Reader TyDefCtx, Error TCError] r =>
String -> [Type] -> Sem r Type
lookupTyDefn String
name [Type]
args Sem r Type -> (Type -> Sem r [Type]) -> Sem r [Type]
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
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 a. a -> Sem r a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> Sem r a
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 a. a -> Sem r a
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 :: forall a. 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 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r Type
ensureConstr1 Con
c Type
ty Either Term Pattern
targ = do
  [Type]
tys <- Con -> Type -> Either Term Pattern -> Sem r [Type]
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
targ
  case [Type]
tys of
    [Type
ty1] -> Type -> Sem r Type
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r (Type, Type)
ensureConstr2 Con
c Type
ty Either Term Pattern
targ = do
  [Type]
tys <- Con -> Type -> Either Term Pattern -> Sem r [Type]
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
targ
  case [Type]
tys of
    [Type
ty1, Type
ty2] -> (Type, Type) -> Sem r (Type, Type)
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
Infer Either Term Pattern
_ = [Mode] -> Sem r [Mode]
forall a. a -> Sem r a
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 TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Type -> Either Term Pattern -> Sem r [Type]
ensureConstr Con
c Type
ty Either Term Pattern
tp

-- | A variant of 'ensureConstrMode' that expects to get a single
--   'Mode' and throws an error if it encounters any other number.
ensureConstrMode1 ::
  Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
  Con ->
  Mode ->
  Either Term Pattern ->
  Sem r Mode
ensureConstrMode1 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r Mode
ensureConstrMode1 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- Con -> Mode -> Either Term Pattern -> Sem r [Mode]
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
m Either Term Pattern
targ
  case [Mode]
ms of
    [Mode
m1] -> Mode -> Sem r Mode
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)
ensureConstrMode2 Con
c Mode
m Either Term Pattern
targ = do
  [Mode]
ms <- Con -> Mode -> Either Term Pattern -> Sem r [Mode]
forall (r :: EffectRow).
Members
  '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
Con -> Mode -> Either Term Pattern -> Sem r [Mode]
ensureConstrMode Con
c Mode
m Either Term Pattern
targ
  case [Mode]
ms of
    [Mode
m1, Mode
m2] -> (Mode, Mode) -> Sem r (Mode, Mode)
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Member (Writer Constraint) r =>
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 a. a -> Sem r a
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

------------------------------------------------------------
-- Subtyping
------------------------------------------------------------

isSubPolyType ::
  Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
  PolyType ->
  PolyType ->
  Sem r Bool
isSubPolyType :: forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
PolyType -> PolyType -> Sem r Bool
isSubPolyType (Forall Bind [Name Type] Type
b1) (Forall Bind [Name Type] Type
b2) = do
  ([Name Type]
as1, Type
ty1) <- 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
b1
  ([Name Type]
as2, Type
ty2) <- 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
b2
  let c :: Constraint
c = 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]
as1 (Type -> Type -> Constraint
CSub Type
ty1 ([(Name Type, Type)] -> Type -> Type
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs ([Name Type] -> [Type] -> [(Name Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name Type]
as2 ((Name Type -> Type) -> [Name Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name Type -> Type
TyVar [Name Type]
as1)) Type
ty2)))
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"======================================================================"
  Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug Sem r (Doc ann)
"Checking subtyping..."
  PolyType -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty (Bind [Name Type] Type -> PolyType
Forall Bind [Name Type] Type
b1)
  PolyType -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) r, Pretty t) =>
t -> Sem r ()
debugPretty (Bind [Name Type] Type -> PolyType
Forall Bind [Name Type] Type
b2)
  Either SolveError (NonEmpty S)
ss <- Sem (Error SolveError : r) (NonEmpty S)
-> Sem r (Either SolveError (NonEmpty S))
forall e (r :: EffectRow) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError (SolutionLimit
-> Sem (State SolutionLimit : Error SolveError : r) (NonEmpty S)
-> Sem (Error SolveError : r) (NonEmpty S)
forall s (r :: EffectRow) a. s -> Sem (State s : r) a -> Sem r a
evalState (Int -> SolutionLimit
SolutionLimit Int
1) (Constraint
-> Sem (State SolutionLimit : Error SolveError : r) (NonEmpty S)
forall ann (r :: EffectRow).
Members
  '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx,
    State SolutionLimit]
  r =>
Constraint -> Sem r (NonEmpty S)
solveConstraint Constraint
c))
  Bool -> Sem r Bool
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ((SolveError -> Bool)
-> (NonEmpty S -> Bool) -> Either SolveError (NonEmpty S) -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Bool -> SolveError -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Bool
not (Bool -> Bool) -> (NonEmpty S -> Bool) -> NonEmpty S -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty S -> Bool
forall a. NonEmpty a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null) Either SolveError (NonEmpty S)
ss)

thin :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType)
thin :: forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
NonEmpty PolyType -> Sem r (NonEmpty PolyType)
thin = ([PolyType] -> NonEmpty PolyType)
-> Sem r [PolyType] -> Sem r (NonEmpty PolyType)
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [PolyType] -> NonEmpty PolyType
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList (Sem r [PolyType] -> Sem r (NonEmpty PolyType))
-> (NonEmpty PolyType -> Sem r [PolyType])
-> NonEmpty PolyType
-> Sem r (NonEmpty PolyType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PolyType] -> Sem r [PolyType]
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
[PolyType] -> Sem r [PolyType]
thin' ([PolyType] -> Sem r [PolyType])
-> (NonEmpty PolyType -> [PolyType])
-> NonEmpty PolyType
-> Sem r [PolyType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty PolyType -> [PolyType]
forall a. NonEmpty a -> [a]
NE.toList

-- Intuitively, this will always return a nonempty list given a nonempty list as input;
-- we could probably rewrite it in terms of NonEmpty combinators but it's more effort than
-- I cared to spend at the moment.
thin' :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => [PolyType] -> Sem r [PolyType]
thin' :: forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
[PolyType] -> Sem r [PolyType]
thin' [] = [PolyType] -> Sem r [PolyType]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
thin' (PolyType
ty : [PolyType]
tys) = do
  Bool
ss <- [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> Sem r [Bool] -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PolyType -> Sem r Bool) -> [PolyType] -> Sem r [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PolyType -> PolyType -> Sem r Bool
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
PolyType -> PolyType -> Sem r Bool
`isSubPolyType` PolyType
ty) [PolyType]
tys
  if Bool
ss
    then [PolyType] -> Sem r [PolyType]
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
[PolyType] -> Sem r [PolyType]
thin' [PolyType]
tys
    else do
      [PolyType]
tys' <- (PolyType -> Sem r Bool) -> [PolyType] -> Sem r [PolyType]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Bool -> Bool) -> Sem r Bool -> Sem r Bool
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (Sem r Bool -> Sem r Bool)
-> (PolyType -> Sem r Bool) -> PolyType -> Sem r Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PolyType
ty PolyType -> PolyType -> Sem r Bool
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
PolyType -> PolyType -> Sem r Bool
`isSubPolyType`)) [PolyType]
tys
      (PolyType
ty PolyType -> [PolyType] -> [PolyType]
forall a. a -> [a] -> [a]
:) ([PolyType] -> [PolyType]) -> Sem r [PolyType] -> Sem r [PolyType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PolyType] -> Sem r [PolyType]
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
[PolyType] -> Sem r [PolyType]
thin' [PolyType]
tys'