{- |
Module      :  ./HasCASL/TypeCheck.hs
Description :  type checking terms and program equations
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

type inference based on

<http://www.cs.fiu.edu/~smithg/papers/>

Principal Type Schemes for Functional Programs with Overloading and
Subtyping, Geoffrey S. Smith, Science of Computer Programming 23(2-3),
pp. 197-226, December 1994
-}

module HasCASL.TypeCheck
    ( typeCheck
    , resolveTerm
    ) where

import HasCASL.Unify
import HasCASL.VarDecl
import HasCASL.As
import HasCASL.Builtin
import HasCASL.FoldType
import HasCASL.Le
import HasCASL.PrintLe
import HasCASL.AsUtils
import HasCASL.MixAna
import HasCASL.TypeAna
import HasCASL.MapTerm
import HasCASL.FoldTerm
import HasCASL.Constrain
import HasCASL.ProgEq
import HasCASL.MinType

import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.Id
import Common.GlobalAnnotations
import Common.Result
import Common.DocUtils
import Common.Lib.State

import Data.Maybe (catMaybes)
import Control.Monad (when, unless)

substTerm :: Subst -> Term -> Term
substTerm :: Subst -> Term -> Term
substTerm s :: Subst
s = Rename -> Term -> Term
mapTerm ((Id, TypeScheme) -> (Id, TypeScheme)
forall a. a -> a
id, Subst -> Type -> Type
subst Subst
s)

-- | mixfix and type resolution
resolveTerm :: Type -> Term -> State Env (Maybe Term)
resolveTerm :: Type -> Term -> State Env (Maybe Term)
resolveTerm mt :: Type
mt trm :: Term
trm = do
    Maybe Term
mtrm <- Term -> State Env (Maybe Term)
resolve Term
trm
    case Maybe Term
mtrm of
      Nothing -> Maybe Term -> State Env (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
      Just t :: Term
t -> Type -> Term -> State Env (Maybe Term)
typeCheck Type
mt Term
t

-- | get a constraint from a type argument instantiated with a type
mkConstraint :: (Type, VarKind) -> Constrain
mkConstraint :: (Type, VarKind) -> Constrain
mkConstraint (ty :: Type
ty, vk :: VarKind
vk) = case VarKind
vk of
    MissingKind -> [Char] -> Constrain
forall a. HasCallStack => [Char] -> a
error "mkConstraint"
    VarKind k :: Kind
k -> Type -> Kind -> Constrain
Kinding Type
ty Kind
k
    Downset super :: Type
super -> Type -> Type -> Constrain
Subtyping Type
ty Type
super

instantiate :: [Type] -> TypeScheme
            -> State Env (Maybe (Type, [(Type, VarKind)]))
instantiate :: [Type] -> TypeScheme -> State Env (Maybe (Type, [(Type, VarKind)]))
instantiate tys :: [Type]
tys sc :: TypeScheme
sc@(TypeScheme tArgs :: [TypeArg]
tArgs t :: Type
t _) =
    if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys Bool -> Bool -> Bool
|| [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [TypeArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg]
tArgs then
         if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys then ((Type, [(Type, VarKind)]) -> Maybe (Type, [(Type, VarKind)]))
-> State Env (Type, [(Type, VarKind)])
-> State Env (Maybe (Type, [(Type, VarKind)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type, [(Type, VarKind)]) -> Maybe (Type, [(Type, VarKind)])
forall a. a -> Maybe a
Just (State Env (Type, [(Type, VarKind)])
 -> State Env (Maybe (Type, [(Type, VarKind)])))
-> State Env (Type, [(Type, VarKind)])
-> State Env (Maybe (Type, [(Type, VarKind)]))
forall a b. (a -> b) -> a -> b
$ State Int (Type, [(Type, VarKind)])
-> State Env (Type, [(Type, VarKind)])
forall a. State Int a -> State Env a
toEnvState (State Int (Type, [(Type, VarKind)])
 -> State Env (Type, [(Type, VarKind)]))
-> State Int (Type, [(Type, VarKind)])
-> State Env (Type, [(Type, VarKind)])
forall a b. (a -> b) -> a -> b
$ TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst TypeScheme
sc
         else do
             [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> [Type] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint ("for type scheme '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                 Type -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Type
t "' wrong length of instantiation list") [Type]
tys]
             Maybe (Type, [(Type, VarKind)])
-> State Env (Maybe (Type, [(Type, VarKind)]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Type, [(Type, VarKind)])
forall a. Maybe a
Nothing
        else let s :: Subst
s = [(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [-1, -2 ..] [Type]
tys
             in Maybe (Type, [(Type, VarKind)])
-> State Env (Maybe (Type, [(Type, VarKind)]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Type, [(Type, VarKind)])
 -> State Env (Maybe (Type, [(Type, VarKind)])))
-> Maybe (Type, [(Type, VarKind)])
-> State Env (Maybe (Type, [(Type, VarKind)]))
forall a b. (a -> b) -> a -> b
$ (Type, [(Type, VarKind)]) -> Maybe (Type, [(Type, VarKind)])
forall a. a -> Maybe a
Just
                (Subst -> Type -> Type
substGen Subst
s Type
t, [Type] -> [VarKind] -> [(Type, VarKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
tys ([VarKind] -> [(Type, VarKind)]) -> [VarKind] -> [(Type, VarKind)]
forall a b. (a -> b) -> a -> b
$ (TypeArg -> VarKind) -> [TypeArg] -> [VarKind]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> TypeArg -> VarKind
substTypeArg Subst
s) [TypeArg]
tArgs)

instOpInfo :: [Type] -> OpInfo
           -> State Env (Maybe (Type, [Type], Constraints, OpInfo))
instOpInfo :: [Type]
-> OpInfo -> State Env (Maybe (Type, [Type], Constraints, OpInfo))
instOpInfo tys :: [Type]
tys oi :: OpInfo
oi = do
     Maybe (Type, [(Type, VarKind)])
m <- [Type] -> TypeScheme -> State Env (Maybe (Type, [(Type, VarKind)]))
instantiate [Type]
tys (TypeScheme -> State Env (Maybe (Type, [(Type, VarKind)])))
-> TypeScheme -> State Env (Maybe (Type, [(Type, VarKind)]))
forall a b. (a -> b) -> a -> b
$ OpInfo -> TypeScheme
opType OpInfo
oi
     Maybe (Type, [Type], Constraints, OpInfo)
-> State Env (Maybe (Type, [Type], Constraints, OpInfo))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Type, [Type], Constraints, OpInfo)
 -> State Env (Maybe (Type, [Type], Constraints, OpInfo)))
-> Maybe (Type, [Type], Constraints, OpInfo)
-> State Env (Maybe (Type, [Type], Constraints, OpInfo))
forall a b. (a -> b) -> a -> b
$ case Maybe (Type, [(Type, VarKind)])
m of
       Just (ty :: Type
ty, cl :: [(Type, VarKind)]
cl) ->
           (Type, [Type], Constraints, OpInfo)
-> Maybe (Type, [Type], Constraints, OpInfo)
forall a. a -> Maybe a
Just (Type
ty, ((Type, VarKind) -> Type) -> [(Type, VarKind)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, VarKind) -> Type
forall a b. (a, b) -> a
fst [(Type, VarKind)]
cl, [Constrain] -> Constraints
forall a. Ord a => [a] -> Set a
Set.fromList ([Constrain] -> Constraints) -> [Constrain] -> Constraints
forall a b. (a -> b) -> a -> b
$ ((Type, VarKind) -> Constrain) -> [(Type, VarKind)] -> [Constrain]
forall a b. (a -> b) -> [a] -> [b]
map (Type, VarKind) -> Constrain
mkConstraint [(Type, VarKind)]
cl, OpInfo
oi)
       Nothing -> Maybe (Type, [Type], Constraints, OpInfo)
forall a. Maybe a
Nothing

{- This function has the problem that the type of an earlier component may
   restrict the types of following components too much. -}
checkList :: Bool -> [Maybe Type] -> [Term]
          -> State Env [(Subst, Constraints, [Type], [Term])]
checkList :: Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList isP :: Bool
isP mtys :: [Maybe Type]
mtys trms :: [Term]
trms = case ([Maybe Type]
mtys, [Term]
trms) of
    (ty :: Maybe Type
ty : rty :: [Maybe Type]
rty, trm :: Term
trm : rt :: [Term]
rt) -> do
      [(Subst, Constraints, Type, Term)]
fts0 <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
isP Maybe Type
ty Term
trm
      [(Subst, Constraints, Type, Term)]
fts <- Bool
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
reduce Bool
True [(Subst, Constraints, Type, Term)]
fts0
      [[(Subst, Constraints, [Type], [Term])]]
combs <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, [Type], [Term])])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, [Type], [Term])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (sf :: Subst
sf, cs :: Constraints
cs, tyf :: Type
tyf, tf :: Term
tf) -> do
                      Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
                      Map Id VarDefn -> State Env ()
putLocalVars (Map Id VarDefn -> State Env ()) -> Map Id VarDefn -> State Env ()
forall a b. (a -> b) -> a -> b
$ Subst -> Map Id VarDefn -> Map Id VarDefn
substVarTypes Subst
sf Map Id VarDefn
vs
                      [(Subst, Constraints, [Type], [Term])]
rts <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
isP ((Maybe Type -> Maybe Type) -> [Maybe Type] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> Type -> Type
subst Subst
sf)) [Maybe Type]
rty) [Term]
rt
                      Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
                      [(Subst, Constraints, [Type], [Term])]
-> State Env [(Subst, Constraints, [Type], [Term])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, [Type], [Term])]
 -> State Env [(Subst, Constraints, [Type], [Term])])
-> [(Subst, Constraints, [Type], [Term])]
-> State Env [(Subst, Constraints, [Type], [Term])]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, [Type], [Term])
 -> (Subst, Constraints, [Type], [Term]))
-> [(Subst, Constraints, [Type], [Term])]
-> [(Subst, Constraints, [Type], [Term])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (sr :: Subst
sr, cr :: Constraints
cr, tys :: [Type]
tys, tts :: [Term]
tts) ->
                             (Subst -> Subst -> Subst
compSubst Subst
sf Subst
sr,
                              Subst -> Constraints -> Constraints
substC Subst
sr Constraints
cs Constraints -> Constraints -> Constraints
`joinC` Constraints
cr,
                              Subst -> Type -> Type
subst Subst
sr Type
tyf Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys,
                                     Term
tf Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
tts)) [(Subst, Constraints, [Type], [Term])]
rts) [(Subst, Constraints, Type, Term)]
fts
      [(Subst, Constraints, [Type], [Term])]
-> State Env [(Subst, Constraints, [Type], [Term])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, [Type], [Term])]
 -> State Env [(Subst, Constraints, [Type], [Term])])
-> [(Subst, Constraints, [Type], [Term])]
-> State Env [(Subst, Constraints, [Type], [Term])]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, [Type], [Term])]]
-> [(Subst, Constraints, [Type], [Term])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, [Type], [Term])]]
combs
    _ -> [(Subst, Constraints, [Type], [Term])]
-> State Env [(Subst, Constraints, [Type], [Term])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst
eps, Constraints
noC, [], [])]

-- | reduce a substitution
reduceR :: Bool -> Env -> (Subst, Constraints, Type, Term)
        -> State Int (Result (Subst, Constraints, Type, Term))
reduceR :: Bool
-> Env
-> (Subst, Constraints, Type, Term)
-> State Int (Result (Subst, Constraints, Type, Term))
reduceR doMono :: Bool
doMono te :: Env
te (s :: Subst
s, cr :: Constraints
cr, ty :: Type
ty, tr :: Term
tr) = do
    Result ds0 :: [Diagnosis]
ds0 mc :: Maybe (Subst, Constraints)
mc <- Bool
-> Env
-> Constraints
-> Maybe Type
-> State Int (Result (Subst, Constraints))
shapeRelAndSimplify Bool
True Env
te Constraints
cr
      (Maybe Type -> State Int (Result (Subst, Constraints)))
-> Maybe Type -> State Int (Result (Subst, Constraints))
forall a b. (a -> b) -> a -> b
$ if Bool
doMono then Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty else Maybe Type
forall a. Maybe a
Nothing
    let ds :: [Diagnosis]
ds = (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Diagnosis -> Diagnosis
forall a. (GetRange a, Pretty a) => a -> Diagnosis -> Diagnosis
improveDiag Term
tr) [Diagnosis]
ds0
    Result (Subst, Constraints, Type, Term)
-> State Int (Result (Subst, Constraints, Type, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Subst, Constraints, Type, Term)
 -> State Int (Result (Subst, Constraints, Type, Term)))
-> Result (Subst, Constraints, Type, Term)
-> State Int (Result (Subst, Constraints, Type, Term))
forall a b. (a -> b) -> a -> b
$ case Maybe (Subst, Constraints)
mc of
        Nothing -> [Diagnosis]
-> Maybe (Subst, Constraints, Type, Term)
-> Result (Subst, Constraints, Type, Term)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Subst, Constraints, Type, Term)
forall a. Maybe a
Nothing
        Just (s1 :: Subst
s1, qs :: Constraints
qs) -> let
          s2 :: Subst
s2 = Subst -> Subst -> Subst
compSubst Subst
s Subst
s1
          in [Diagnosis]
-> Maybe (Subst, Constraints, Type, Term)
-> Result (Subst, Constraints, Type, Term)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds (Maybe (Subst, Constraints, Type, Term)
 -> Result (Subst, Constraints, Type, Term))
-> Maybe (Subst, Constraints, Type, Term)
-> Result (Subst, Constraints, Type, Term)
forall a b. (a -> b) -> a -> b
$ (Subst, Constraints, Type, Term)
-> Maybe (Subst, Constraints, Type, Term)
forall a. a -> Maybe a
Just
             (Subst
s2, Constraints
qs, Subst -> Type -> Type
subst Subst
s1 Type
ty, Subst -> Term -> Term
substTerm Subst
s2 Term
tr)

-- | reduce a substitution
reduce :: Bool -> [(Subst, Constraints, Type, Term)]
       -> State Env [(Subst, Constraints, Type, Term)]
reduce :: Bool
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
reduce doMono :: Bool
doMono alts :: [(Subst, Constraints, Type, Term)]
alts = do
       Env
te <- State Env Env
forall s. State s s
get
       [[(Subst, Constraints, Type, Term)]]
combs <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ alt :: (Subst, Constraints, Type, Term)
alt -> do
         Result ds :: [Diagnosis]
ds mc :: Maybe (Subst, Constraints, Type, Term)
mc <- State Int (Result (Subst, Constraints, Type, Term))
-> State Env (Result (Subst, Constraints, Type, Term))
forall a. State Int a -> State Env a
toEnvState (State Int (Result (Subst, Constraints, Type, Term))
 -> State Env (Result (Subst, Constraints, Type, Term)))
-> State Int (Result (Subst, Constraints, Type, Term))
-> State Env (Result (Subst, Constraints, Type, Term))
forall a b. (a -> b) -> a -> b
$ Bool
-> Env
-> (Subst, Constraints, Type, Term)
-> State Int (Result (Subst, Constraints, Type, Term))
reduceR Bool
doMono Env
te (Subst, Constraints, Type, Term)
alt
         [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
         case Maybe (Subst, Constraints, Type, Term)
mc of
           Nothing -> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           Just q :: (Subst, Constraints, Type, Term)
q -> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst, Constraints, Type, Term)
q]) [(Subst, Constraints, Type, Term)]
alts
       [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
combs

checkForUninstantiatedVars :: GlobalAnnos -> Term -> Range -> State Env ()
checkForUninstantiatedVars :: GlobalAnnos -> Term -> Range -> State Env ()
checkForUninstantiatedVars ga :: GlobalAnnos
ga t :: Term
t p :: Range
p = let
  tys :: [Type]
tys = Term -> [Type]
getAllVarTypes Term
t
  in Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags
    [(DiagKind -> [Char] -> [Id] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error ("in term '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> Term -> [Char] -> [Char]
forall a. Pretty a => GlobalAnnos -> a -> [Char] -> [Char]
showGlobalDoc GlobalAnnos
ga Term
t
                    "'\n are uninstantiated type variables")
      ([Id] -> Diagnosis) -> [Id] -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
      ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Type -> Set Id) -> [Type] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> (Type -> [Id]) -> Type -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Id]
freeTVarIds) [Type]
tys)
     {diagPos :: Range
diagPos = Range
p}]

simplifyTypedTerms :: Env -> Term -> Term
simplifyTypedTerms :: Env -> Term -> Term
simplifyTypedTerms e :: Env
e = FoldRec Term ProgEq -> Term -> Term
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec Term ProgEq
mapRec
  { foldTypedTerm :: Term -> Term -> TypeQual -> Type -> Range -> Term
foldTypedTerm = \ _ nt :: Term
nt q :: TypeQual
q ty :: Type
ty ps :: Range
ps ->
      let ntyped :: Term
ntyped = Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
nt TypeQual
q Type
ty Range
ps
          ityped :: Term
ityped = Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
nt TypeQual
Inferred Type
ty Range
ps
      in case Term -> Maybe Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
nt of
        Nothing -> Term
ntyped
        Just ty2 :: Type
ty2 -> let isSubT :: Bool
isSubT = Env -> Type -> Type -> Bool
lesserType Env
e Type
ty2 Type
ty in
          case TypeQual
q of
            InType | Bool
isSubT -> Id -> Range -> Term
unitTerm Id
trueId Range
ps
            _ -> case Term
nt of
              TypedTerm nt2 :: Term
nt2 q2 :: TypeQual
q2 _ _
               | TypeQual
q2 TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
AsType Bool -> Bool -> Bool
&& TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeQual
InType Bool -> Bool -> Bool
&& Env -> Type -> Type -> Bool
lesserType Env
e Type
ty Type
ty2
                  -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
nt2 TypeQual
q2 Type
ty Range
ps
               | TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
AsType Bool -> Bool -> Bool
&& TypeQual -> [TypeQual] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem TypeQual
q2 [TypeQual
OfType, TypeQual
Inferred] Bool -> Bool -> Bool
&& Bool
isSubT
                   -> Term
ityped
               | Bool
otherwise -> Term
ntyped
              _ -> if TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
AsType Bool -> Bool -> Bool
&& Bool
isSubT then Term
ityped else Term
ntyped }

-- | type checking a term
typeCheck :: Type -> Term -> State Env (Maybe Term)
typeCheck :: Type -> Term -> State Env (Maybe Term)
typeCheck exTy :: Type
exTy trm :: Term
trm =
    do [(Subst, Constraints, Type, Term)]
alts0 <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
False (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
exTy) Term
trm
       [(Subst, Constraints, Type, Term)]
alts <- Bool
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
reduce Bool
True [(Subst, Constraints, Type, Term)]
alts0
       Env
te <- State Env Env
forall s. State s s
get
       let p :: Range
p = Term -> Range
forall a. GetRange a => a -> Range
getRange Term
trm
           ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
te
       case Env
-> ((Subst, Constraints, Type, Term) -> (Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a. Env -> (a -> (Type, Term)) -> [a] -> [a]
typeNub Env
te (Subst, Constraints, Type, Term) -> (Type, Term)
forall a b c d. (a, b, c, d) -> (c, d)
q2p [(Subst, Constraints, Type, Term)]
alts of
         [] -> do
           [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> [Char] -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Error "no typing for" Term
trm]
           Maybe Term -> State Env (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
         [(_, rcs :: Constraints
rcs, ty :: Type
ty, t :: Term
t)] -> do
           Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Constraints -> Bool
forall a. Set a -> Bool
Set.null Constraints
rcs)
                 (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [(DiagKind -> [Char] -> Constraints -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error ("in term '"
                             [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> Term -> [Char] -> [Char]
forall a. Pretty a => GlobalAnnos -> a -> [Char] -> [Char]
showGlobalDoc GlobalAnnos
ga Term
t "' of type '"
                             [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Type
ty "'\n unresolved constraints")
                                 Constraints
rcs) {diagPos :: Range
diagPos = Range
p}]
           GlobalAnnos -> Term -> Range -> State Env ()
checkForUninstantiatedVars GlobalAnnos
ga Term
t Range
p
           Maybe Term -> State Env (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> State Env (Maybe Term))
-> Maybe Term -> State Env (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Term
simplifyTypedTerms Env
te Term
t
         falts :: [(Subst, Constraints, Type, Term)]
falts -> do
               [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Error
                         ("ambiguous typings\n " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                          ([Char] -> [Char])
-> ((Int, Term) -> [Char] -> [Char])
-> [(Int, Term)]
-> [Char]
-> [Char]
forall a.
([Char] -> [Char])
-> (a -> [Char] -> [Char]) -> [a] -> [Char] -> [Char]
showSepList ("\n " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
                          ( \ (n :: Int
n, t :: Term
t) -> Int -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows Int
n ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (". " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Term
t)
                          ([Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [1 .. (5 :: Int)] ([Term] -> [(Int, Term)]) -> [Term] -> [(Int, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term) -> Term)
-> [(Subst, Constraints, Type, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, _, _, t :: Term
t) ->
                                          Term
t) [(Subst, Constraints, Type, Term)]
falts) "")
                            Range
p]
               Maybe Term -> State Env (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing

freshTypeVar :: Term -> State Env Type
freshTypeVar :: Term -> State Env Type
freshTypeVar t :: Term
t =
    do (var :: Id
var, c :: Int
c) <- State Int (Id, Int) -> State Env (Id, Int)
forall a. State Int a -> State Env a
toEnvState (State Int (Id, Int) -> State Env (Id, Int))
-> State Int (Id, Int) -> State Env (Id, Int)
forall a b. (a -> b) -> a -> b
$ Id -> State Int (Id, Int)
freshVar (Id -> State Int (Id, Int)) -> Id -> State Int (Id, Int)
forall a b. (a -> b) -> a -> b
$ [Token] -> [Id] -> Range -> Id
Id [] [] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t
       Type -> State Env Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Env Type) -> Type -> State Env Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
var RawKind
rStar Int
c

substVarTypes :: Subst -> Map.Map Id VarDefn -> Map.Map Id VarDefn
substVarTypes :: Subst -> Map Id VarDefn -> Map Id VarDefn
substVarTypes s :: Subst
s = (VarDefn -> VarDefn) -> Map Id VarDefn -> Map Id VarDefn
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ( \ (VarDefn t :: Type
t) -> Type -> VarDefn
VarDefn (Type -> VarDefn) -> Type -> VarDefn
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
subst Subst
s Type
t)

warnEmpty :: Maybe Type -> Term -> [a] -> State Env ()
warnEmpty :: Maybe Type -> Term -> [a] -> State Env ()
warnEmpty mt :: Maybe Type
mt trm :: Term
trm res :: [a]
res = do
    GlobalAnnos
ga <- (Env -> GlobalAnnos) -> State Env GlobalAnnos
forall s a. (s -> a) -> State s a
gets Env -> GlobalAnnos
globAnnos
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
res) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> [Char] -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Hint ("untypeable term" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      case Maybe Type
mt of
        Nothing -> ""
        Just ty :: Type
ty -> " (with type: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> Type -> [Char] -> [Char]
forall a. Pretty a => GlobalAnnos -> a -> [Char] -> [Char]
showGlobalDoc GlobalAnnos
ga Type
ty ")") Term
trm]

-- | infer type of application, consider lifting for lazy types
inferAppl :: Bool -> Range -> Term -> Term
          -> State Env [(Subst, Constraints, Type, Term)]
inferAppl :: Bool
-> Range
-> Term
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferAppl isP :: Bool
isP ps :: Range
ps t1 :: Term
t1 t2 :: Term
t2 = do
    [(Subst, Constraints, Type, Term)]
ops <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
isP Term
t1
    Maybe Type
-> Term -> [(Subst, Constraints, Type, Term)] -> State Env ()
forall a. Maybe Type -> Term -> [a] -> State Env ()
warnEmpty Maybe Type
forall a. Maybe a
Nothing Term
t1 [(Subst, Constraints, Type, Term)]
ops
    Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
    Env
e <- State Env Env
forall s. State s s
get
    [[(Subst, Constraints, Type, Term)]]
combs <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (sf :: Subst
sf, cf :: Constraints
cf, funty :: Type
funty, tf :: Term
tf) -> do
        (ok :: Bool
ok, sfty :: Maybe Type
sfty, frty :: Type
frty, sub :: Bool
sub) <- case Type -> (Type, [Type])
getTypeAppl Type
funty of
                          (topTy :: Type
topTy, [paty :: Type
paty, prty :: Type
prty]) |
                            Env -> Type -> Type -> Bool
lesserType Env
e Type
topTy (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ Arrow -> Type
toFunType Arrow
PFunArr ->
                                (Bool, Maybe Type, Type, Bool)
-> State Env (Bool, Maybe Type, Type, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Type -> Maybe Type
forall a. a -> Maybe a
Just Type
paty, Type
prty, Bool
False)
                          (topTy :: Type
topTy, [prty :: Type
prty]) |
                            Env -> Type -> Type -> Bool
lesserType Env
e Type
topTy Type
lazyTypeConstr ->
                                (Bool, Maybe Type, Type, Bool)
-> State Env (Bool, Maybe Type, Type, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Type -> Maybe Type
forall a. a -> Maybe a
Just Type
unitType, Type
prty, Bool
False)
                          (TypeName _ _ c :: Int
c, []) | Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> do
                            Type
rty <- Term -> State Env Type
freshTypeVar Term
t1
                            (Bool, Maybe Type, Type, Bool)
-> State Env (Bool, Maybe Type, Type, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Maybe Type
forall a. Maybe a
Nothing, Type
rty, Bool
True)
                          _ -> (Bool, Maybe Type, Type, Bool)
-> State Env (Bool, Maybe Type, Type, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe Type
forall a. Maybe a
Nothing, Type
funty, Bool
False)
        if Bool
ok then do
                Map Id VarDefn -> State Env ()
putLocalVars (Map Id VarDefn -> State Env ()) -> Map Id VarDefn -> State Env ()
forall a b. (a -> b) -> a -> b
$ Subst -> Map Id VarDefn -> Map Id VarDefn
substVarTypes Subst
sf Map Id VarDefn
vs
                [(Subst, Constraints, Type, Term)]
args <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
isP Maybe Type
sfty Term
t2
                Maybe Type
-> Term -> [(Subst, Constraints, Type, Term)] -> State Env ()
forall a. Maybe Type -> Term -> [a] -> State Env ()
warnEmpty Maybe Type
sfty Term
t2 [(Subst, Constraints, Type, Term)]
args
                Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
                [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (sa :: Subst
sa, ca :: Constraints
ca, arty :: Type
arty, ta :: Term
ta) ->
                        let nTy :: Type
nTy = Subst -> Type -> Type
subst Subst
sa Type
frty in
                          (Subst -> Subst -> Subst
compSubst Subst
sf Subst
sa, (if Bool
sub then
                               Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping (Subst -> Type -> Type
subst Subst
sa Type
funty)
                                (Type -> Constrain) -> Type -> Constrain
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType Type
arty Arrow
PFunArr Type
nTy) else Constraints -> Constraints
forall a. a -> a
id)
                              (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Constraints -> Constraints -> Constraints
joinC Constraints
ca (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Subst -> Constraints -> Constraints
substC Subst
sa Constraints
cf, Type
nTy,
                            Term -> TypeQual -> Type -> Range -> Term
TypedTerm (Term -> Term -> Range -> Term
ApplTerm Term
tf Term
ta Range
ps)
                            TypeQual
Inferred Type
nTy Range
ps)) [(Subst, Constraints, Type, Term)]
args
            else [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) [(Subst, Constraints, Type, Term)]
ops
    Bool
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
reduce Bool
False ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
combs

getAllVarTypes :: Term -> [Type]
getAllVarTypes :: Term -> [Type]
getAllVarTypes = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Int, (Id, RawKind))] -> Bool)
-> (Type -> [(Int, (Id, RawKind))]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [(Int, (Id, RawKind))]
freeTVars) ([Type] -> [Type]) -> (Term -> [Type]) -> Term -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Type]
getAllTypes

mkTypedTerm :: Term -> Type -> Term
mkTypedTerm :: Term -> Type -> Term
mkTypedTerm trm :: Term
trm ty :: Type
ty = case Term
trm of
    TupleTerm ts :: [Term]
ts ps :: Range
ps | Bool -> Bool
not ([Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts) -> let
      n :: Int
n = [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts
      (topTy :: Type
topTy, tArgs :: [Type]
tArgs) = Type -> (Type, [Type])
getTypeAppl Type
ty
      in if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 Bool -> Bool -> Bool
&& Type
topTy Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Range -> Type
toProdType Int
n Range
ps
             Bool -> Bool -> Bool
&& [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tArgs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n then
      [Term] -> Range -> Term
TupleTerm ((Term -> Type -> Term) -> [Term] -> [Type] -> [Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Term -> Type -> Term
mkTypedTerm [Term]
ts [Type]
tArgs) Range
ps
      else Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
trm TypeQual
Inferred Type
ty Range
ps
    LetTerm br :: LetBrand
br eqs :: [ProgEq]
eqs inTrm :: Term
inTrm ps :: Range
ps -> LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
br [ProgEq]
eqs (Term -> Type -> Term
mkTypedTerm Term
inTrm Type
ty) Range
ps
    QuantifiedTerm quant :: Quantifier
quant decls :: [GenVarDecl]
decls t :: Term
t ps :: Range
ps ->
        Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
quant [GenVarDecl]
decls (Term -> Type -> Term
mkTypedTerm Term
t Type
ty) Range
ps
    _ -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
trm TypeQual
Inferred Type
ty (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
trm

-- | efficiently infer type of a monomorphic tuple term
inferWithMaybeType :: Bool -> Maybe Type -> Term
                   -> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType :: Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType isP :: Bool
isP mt :: Maybe Type
mt trm :: Term
trm = case (Term
trm, Maybe Type
mt) of
    (TupleTerm ts :: [Term]
ts@(_ : _ : _) ps :: Range
ps, Just ty :: Type
ty) -> case Type -> (Type, [Type])
getTypeAppl Type
ty of
        (TypeName i :: Id
i _ _, argTys :: [Type]
argTys@(_ : _ : _)) | Id -> Bool
isProductId Id
i ->
          if [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
argTys then
              if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Int, (Id, RawKind))] -> Bool)
-> (Type -> [(Int, (Id, RawKind))]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [(Int, (Id, RawKind))]
freeTVars) [Type]
argTys then do
                 -- remaining type variables would not become instantiated
                [(Subst, Constraints, [Type], [Term])]
ls <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
isP ((Type -> Maybe Type) -> [Type] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Maybe Type
forall a. a -> Maybe a
Just [Type]
argTys) [Term]
ts
                [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, [Type], [Term])
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, [Type], [Term])]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (su :: Subst
su, cs :: Constraints
cs, tys :: [Type]
tys, trms :: [Term]
trms) ->
                  ( Subst
su, Constraints
cs, [Type] -> Range -> Type
mkProductTypeWithRange [Type]
tys Range
ps
                  , [Term] -> Range -> Term
mkTupleTerm [Term]
trms Range
ps)) [(Subst, Constraints, [Type], [Term])]
ls
              else Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeTypeAux Bool
isP Maybe Type
mt Term
trm
           else [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- fail for tuples of different lengths
        _ -> Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeTypeAux Bool
isP Maybe Type
mt Term
trm
    _ -> Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeTypeAux Bool
isP Maybe Type
mt Term
trm

-- | infer type of term (or a pattern if the Bool is True)
inferWithMaybeTypeAux :: Bool -> Maybe Type -> Term
                   -> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeTypeAux :: Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeTypeAux isP :: Bool
isP mt :: Maybe Type
mt trm :: Term
trm = do
  [(Subst, Constraints, Type, Term)]
rs <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
isP Term
trm
  Env
te <- State Env Env
forall s. State s s
get
  case Maybe Type
mt of
    Nothing -> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst, Constraints, Type, Term)]
rs
    Just inTy :: Type
inTy -> do
        [[(Subst, Constraints, Type, Term)]]
combs <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ q :: (Subst, Constraints, Type, Term)
q@(s :: Subst
s, c :: Constraints
c, ty :: Type
ty, t :: Term
t) -> let nTy :: Type
nTy = Subst -> Type -> Type
subst Subst
s Type
inTy in
            if Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
nTy then [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst, Constraints, Type, Term)
q] else do
            Result ds :: [Diagnosis]
ds mc :: Maybe (Subst, Constraints, Type, Term)
mc <- State Int (Result (Subst, Constraints, Type, Term))
-> State Env (Result (Subst, Constraints, Type, Term))
forall a. State Int a -> State Env a
toEnvState (State Int (Result (Subst, Constraints, Type, Term))
 -> State Env (Result (Subst, Constraints, Type, Term)))
-> State Int (Result (Subst, Constraints, Type, Term))
-> State Env (Result (Subst, Constraints, Type, Term))
forall a b. (a -> b) -> a -> b
$ Bool
-> Env
-> (Subst, Constraints, Type, Term)
-> State Int (Result (Subst, Constraints, Type, Term))
reduceR Bool
False Env
te
              (Subst
s, Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping Type
ty Type
nTy) Constraints
c, Type
nTy, Term -> Type -> Term
mkTypedTerm Term
t Type
nTy)
            case Maybe (Subst, Constraints, Type, Term)
mc of
              Nothing -> do
                [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
                [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
              Just alt :: (Subst, Constraints, Type, Term)
alt -> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst, Constraints, Type, Term)
alt]) [(Subst, Constraints, Type, Term)]
rs
        [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
combs

-- | infer type of term (or a pattern if the Bool is True)
infer :: Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer :: Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer isP :: Bool
isP trm :: Term
trm = do
    Env
e <- State Env Env
forall s. State s s
get
    let tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e
        bs :: Map Id Id
bs = Env -> Map Id Id
binders Env
e
        vs :: Map Id VarDefn
vs = Env -> Map Id VarDefn
localVars Env
e
        ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
e
    case Term
trm of
        qv :: Term
qv@(QualVar (VarDecl _ ty :: Type
ty _ _)) -> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst
eps, Constraints
noC, Type
ty, Term
qv)]
        QualOp br :: OpBrand
br i :: PolyId
i sc :: TypeScheme
sc tys :: [Type]
tys k :: InstKind
k ps :: Range
ps -> do
            Maybe (Type, [Type], Constraints, OpInfo)
ms <- [Type]
-> OpInfo -> State Env (Maybe (Type, [Type], Constraints, OpInfo))
instOpInfo [Type]
tys OpInfo :: TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo { opType :: TypeScheme
opType = TypeScheme
sc
                                        , opAttrs :: Set OpAttr
opAttrs = Set OpAttr
forall a. Set a
Set.empty
                                        , opDefn :: OpDefn
opDefn = OpBrand -> OpDefn
NoOpDefn OpBrand
br }
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ case Maybe (Type, [Type], Constraints, OpInfo)
ms of
                Nothing -> []
                Just (ty :: Type
ty, inst :: [Type]
inst, cs :: Constraints
cs, _) ->
                    let qv :: Term
qv = Term -> TypeQual -> Type -> Range -> Term
TypedTerm (OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
br PolyId
i TypeScheme
sc [Type]
inst InstKind
k Range
ps)
                             TypeQual
Inferred Type
ty Range
ps
                    in [(Subst
eps, Constraints
cs, Type
ty, Term
qv)]
        ResolvedMixTerm i :: Id
i tys :: [Type]
tys ts :: [Term]
ts ps :: Range
ps -> case (Id -> Map Id Id -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Map Id Id
bs, [Term]
ts) of
          (Just j :: Id
j, pat :: Term
pat : rt :: [Term]
rt@(_ : _)) -> case [Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
rt of
            lt :: Term
lt : ft :: [Term]
ft -> Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
isP (Term -> State Env [(Subst, Constraints, Type, Term)])
-> Term -> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
j [Type]
tys
                ([Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term
pat] Partiality
Partial Term
lt Range
ps Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ft) Range
ps
            [] -> [Char] -> State Env [(Subst, Constraints, Type, Term)]
forall a. HasCallStack => [Char] -> a
error "ResolvedMixTerm: binder"
          _ ->
            if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts then case Id -> Map Id VarDefn -> Maybe VarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Map Id VarDefn
vs of
               Just (VarDefn t :: Type
t) ->
                 Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
isP (Term -> State Env [(Subst, Constraints, Type, Term)])
-> Term -> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
i Type
t SeparatorKind
Other Range
ps
               Nothing -> do
                    [Maybe (Type, [Type], Constraints, OpInfo)]
insts <- (OpInfo -> State Env (Maybe (Type, [Type], Constraints, OpInfo)))
-> [OpInfo]
-> State Env [Maybe (Type, [Type], Constraints, OpInfo)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Type]
-> OpInfo -> State Env (Maybe (Type, [Type], Constraints, OpInfo))
instOpInfo [Type]
tys) ([OpInfo] -> State Env [Maybe (Type, [Type], Constraints, OpInfo)])
-> [OpInfo]
-> State Env [Maybe (Type, [Type], Constraints, OpInfo)]
forall a b. (a -> b) -> a -> b
$ Env -> Id -> [OpInfo]
getMinAssumps Env
e Id
i
                    let ls :: [(Subst, Type, [Type], Constraints, OpInfo)]
ls = ((Type, [Type], Constraints, OpInfo)
 -> (Subst, Type, [Type], Constraints, OpInfo))
-> [(Type, [Type], Constraints, OpInfo)]
-> [(Subst, Type, [Type], Constraints, OpInfo)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (ty :: Type
ty, is :: [Type]
is, cs :: Constraints
cs, oi :: OpInfo
oi) ->
                              (Subst
eps, Type
ty, [Type]
is, Constraints
cs, OpInfo
oi)) ([(Type, [Type], Constraints, OpInfo)]
 -> [(Subst, Type, [Type], Constraints, OpInfo)])
-> [(Type, [Type], Constraints, OpInfo)]
-> [(Subst, Type, [Type], Constraints, OpInfo)]
forall a b. (a -> b) -> a -> b
$ [Maybe (Type, [Type], Constraints, OpInfo)]
-> [(Type, [Type], Constraints, OpInfo)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Type, [Type], Constraints, OpInfo)]
insts
                    -- possibly fresh variable
                    [(Subst, Constraints, Type, Term)]
vl <- if Bool
isP Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys Bool -> Bool -> Bool
&& [(Subst, Type, [Type], Constraints, OpInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Subst, Type, [Type], Constraints, OpInfo)]
ls
                          Bool -> Bool -> Bool
&& (Id -> Bool
isSimpleId Id
i Bool -> Bool -> Bool
|| Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Token -> Id
simpleIdToId Token
uTok) then do
                        Type
vty <- Term -> State Env Type
freshTypeVar Term
trm
                        [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return
                          [(Subst
eps, Constraints
noC, Type
vty, VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
i Type
vty SeparatorKind
Other Range
ps)]
                      else do
                        Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Subst, Type, [Type], Constraints, OpInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Subst, Type, [Type], Constraints, OpInfo)]
ls) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$
                          [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "no type found for" Id
i]
                        [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                    [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [(Subst, Constraints, Type, Term)]
vl [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a. [a] -> [a] -> [a]
++ ((Subst, Type, [Type], Constraints, OpInfo)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Type, [Type], Constraints, OpInfo)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map
                      ( \ (s :: Subst
s, ty :: Type
ty, is :: [Type]
is, cs :: Constraints
cs, oi :: OpInfo
oi) ->
                        let od :: OpDefn
od = OpInfo -> OpDefn
opDefn OpInfo
oi
                            br :: OpBrand
br = case OpDefn
od of
                                 NoOpDefn v :: OpBrand
v -> OpBrand
v
                                 Definition v :: OpBrand
v _ -> OpBrand
v
                                 _ -> OpBrand
Op
                            ik :: InstKind
ik = if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys then InstKind
Infer else InstKind
UserGiven
                       in (Subst
s, Constraints
cs, Type
ty, case OpInfo -> TypeScheme
opType OpInfo
oi of
                           sc :: TypeScheme
sc@(TypeScheme [] _ _) ->
                                  OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
br (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
ps) TypeScheme
sc [] InstKind
ik Range
ps
                           sc :: TypeScheme
sc -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm (OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
br (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
ps)
                                            TypeScheme
sc [Type]
is InstKind
ik Range
ps)
                                       TypeQual
Inferred Type
ty Range
ps)) [(Subst, Type, [Type], Constraints, OpInfo)]
ls
            else Bool
-> Range
-> Term
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferAppl Bool
isP Range
ps (Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
i [Type]
tys [] Range
ps)
                 (Term -> State Env [(Subst, Constraints, Type, Term)])
-> Term -> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
mkTupleTerm [Term]
ts Range
ps
        ApplTerm t1 :: Term
t1 t2 :: Term
t2 ps :: Range
ps -> Bool
-> Range
-> Term
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferAppl Bool
isP Range
ps Term
t1 Term
t2
        TupleTerm ts :: [Term]
ts ps :: Range
ps -> if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts then [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst
eps, Constraints
noC, Type
unitType, Term
trm)]
          else do
            [(Subst, Constraints, [Type], [Term])]
ls <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
isP ((Term -> Maybe Type) -> [Term] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Term -> Maybe Type
forall a b. a -> b -> a
const Maybe Type
forall a. Maybe a
Nothing) [Term]
ts) [Term]
ts
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, [Type], [Term])
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, [Type], [Term])]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (su :: Subst
su, cs :: Constraints
cs, tys :: [Type]
tys, trms :: [Term]
trms) ->
              (Subst
su, Constraints
cs, [Type] -> Range -> Type
mkProductTypeWithRange [Type]
tys Range
ps, [Term] -> Range -> Term
mkTupleTerm [Term]
trms Range
ps)) [(Subst, Constraints, [Type], [Term])]
ls
        TypedTerm t :: Term
t qual :: TypeQual
qual ty :: Type
ty ps :: Range
ps ->
            case TypeQual
qual of
                InType -> do
                    Type
vTy <- Term -> State Env Type
freshTypeVar Term
t
                    [(Subst, Constraints, Type, Term)]
rs <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
False Term
t
                    [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s :: Subst
s, cs :: Constraints
cs, typ :: Type
typ, tr :: Term
tr) ->
                           let sTy :: Type
sTy = Subst -> Type -> Type
subst Subst
s Type
ty in
                               ( Subst
s, Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping Type
sTy Type
vTy)
                                     (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping Type
typ Type
vTy) Constraints
cs
                               , Type
unitType, Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
qual Type
sTy Range
ps)) [(Subst, Constraints, Type, Term)]
rs
                AsType -> do
                    Type
vTy <- Term -> State Env Type
freshTypeVar Term
t
                    [(Subst, Constraints, Type, Term)]
rs <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
False Term
t
                    [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s :: Subst
s, cs :: Constraints
cs, typ :: Type
typ, tr :: Term
tr) ->
                        let sTy :: Type
sTy = Subst -> Type -> Type
subst Subst
s Type
ty in
                                ( Subst
s, Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping Type
sTy Type
vTy)
                                       (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Constrain -> Constraints -> Constraints
insertC (Type -> Type -> Constrain
Subtyping Type
typ Type
vTy) Constraints
cs
                                , Type
sTy, Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
qual Type
sTy Range
ps)) [(Subst, Constraints, Type, Term)]
rs
                _ -> do
                    let decl :: Bool
decl = case Term
t of
                          ResolvedMixTerm _ tys :: [Type]
tys ts :: [Term]
ts _
                              | Bool
isP Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys Bool -> Bool -> Bool
&& [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts Bool -> Bool -> Bool
&& TypeQual
qual TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
OfType
                              -> Bool
True
                          _ -> Bool
False
                    [(Subst, Constraints, Type, Term)]
rs <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
isP
                           (if Bool
decl then Maybe Type
forall a. Maybe a
Nothing else Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty) Term
t
                    [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s :: Subst
s, cs :: Constraints
cs, _, tr :: Term
tr) ->
                          let sTy :: Type
sTy = Subst -> Type -> Type
subst Subst
s Type
ty in
                                (Subst
s, Constraints
cs, Type
sTy, case Term
tr of
                                 QualVar (VarDecl vp :: Id
vp _ po :: SeparatorKind
po _)
                                     | Bool
decl -- shadow
                                     -> VarDecl -> Term
QualVar (Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
vp Type
sTy SeparatorKind
po Range
ps)
                                 _ -> if (TypeQual
qual TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
Inferred Bool -> Bool -> Bool
|| case Term
tr of
                                        QualVar _ -> Bool
True
                                        QualOp {} -> Bool
True
                                        TypedTerm _ OfType _ _ -> Bool
True
                                        _ -> Bool
False)
                                        Bool -> Bool -> Bool
&& Bool -> (Type -> Bool) -> Maybe Type -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Type -> Type -> Bool
eqStrippedType Type
sTy)
                                               (Term -> Maybe Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
tr)
                                      then Term
tr
                                      else Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
qual Type
sTy Range
ps)) [(Subst, Constraints, Type, Term)]
rs
        QuantifiedTerm quant :: Quantifier
quant decls :: [GenVarDecl]
decls t :: Term
t ps :: Range
ps -> do
            (GenVarDecl -> State Env ()) -> [GenVarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ GenVarDecl -> State Env ()
addGenVarDecl [GenVarDecl]
decls
            [(Subst, Constraints, Type, Term)]
rs <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
False (Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkLazyType Type
unitType) Term
t
            Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
            TypeMap -> State Env ()
putTypeMap TypeMap
tm
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s :: Subst
s, cs :: Constraints
cs, typ :: Type
typ, tr :: Term
tr) ->
              (Subst
s, Constraints
cs, Type
typ, Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
quant [GenVarDecl]
decls Term
tr Range
ps)) [(Subst, Constraints, Type, Term)]
rs
        LambdaTerm pats :: [Term]
pats part :: Partiality
part resTrm :: Term
resTrm ps :: Range
ps -> do
            [(Subst, Constraints, [Type], [Term])]
ls <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
True ((Term -> Maybe Type) -> [Term] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Term -> Maybe Type
forall a b. a -> b -> a
const Maybe Type
forall a. Maybe a
Nothing) [Term]
pats) [Term]
pats
            [[(Subst, Constraints, Type, Term)]]
rs <- ((Subst, Constraints, [Type], [Term])
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, [Type], [Term])]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ ( s :: Subst
s, cs :: Constraints
cs, patys :: [Type]
patys, nps :: [Term]
nps) -> do
                       (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
nps
                       [(Subst, Constraints, Type, Term)]
es <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
False Term
resTrm
                       Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
                       [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s2 :: Subst
s2, cr :: Constraints
cr, rty :: Type
rty, rtm :: Term
rtm) ->
                                      let s3 :: Subst
s3 = Subst -> Subst -> Subst
compSubst Subst
s Subst
s2
                                          typ :: Type
typ = Type -> Partiality -> [Type] -> Type
getFunType (Subst -> Type -> Type
subst Subst
s Type
rty)
                                             Partiality
part ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
subst Subst
s2) [Type]
patys
                                      in
                                      (Subst
s3, Constraints -> Constraints -> Constraints
joinC (Subst -> Constraints -> Constraints
substC Subst
s2 Constraints
cs) (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Subst -> Constraints -> Constraints
substC Subst
s Constraints
cr
                                      , Type
typ,
                                       Term -> TypeQual -> Type -> Range -> Term
TypedTerm
                                       ([Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term]
nps Partiality
part Term
rtm Range
ps)
                                       TypeQual
Inferred Type
typ Range
ps)) [(Subst, Constraints, Type, Term)]
es) [(Subst, Constraints, [Type], [Term])]
ls
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
rs
        CaseTerm ofTrm :: Term
ofTrm eqs :: [ProgEq]
eqs ps :: Range
ps -> do
            [(Subst, Constraints, Type, Term)]
ts <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
False Term
ofTrm
            Type
rty <- Term -> State Env Type
freshTypeVar Term
trm
            Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Subst, Constraints, Type, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Subst, Constraints, Type, Term)]
ts) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> [Char] -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Hint
                                      "unresolved of-term in case" Term
ofTrm]
            [[(Subst, Constraints, Type, Term)]]
rs <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (s1 :: Subst
s1, cs :: Constraints
cs, oty :: Type
oty, otrm :: Term
otrm) -> do
                 [(Subst, Constraints, Type, Type, [ProgEq])]
es <- Type
-> Type
-> [ProgEq]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
inferCaseEqs Type
oty (Subst -> Type -> Type
subst Subst
s1 Type
rty) [ProgEq]
eqs
                 [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Type, [ProgEq])
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Type, [ProgEq])]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s2 :: Subst
s2, cr :: Constraints
cr, _, ty :: Type
ty, nes :: [ProgEq]
nes) ->
                                (Subst -> Subst -> Subst
compSubst Subst
s1 Subst
s2,
                                 Subst -> Constraints -> Constraints
substC Subst
s2 Constraints
cs Constraints -> Constraints -> Constraints
`joinC` Constraints
cr, Type
ty,
                                 Term -> TypeQual -> Type -> Range -> Term
TypedTerm (Term -> [ProgEq] -> Range -> Term
CaseTerm Term
otrm [ProgEq]
nes Range
ps)
                                 TypeQual
Inferred Type
ty Range
ps)) [(Subst, Constraints, Type, Type, [ProgEq])]
es) [(Subst, Constraints, Type, Term)]
ts
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
rs
        LetTerm br :: LetBrand
br eqs :: [ProgEq]
eqs inTrm :: Term
inTrm ps :: Range
ps -> do
            [(Subst, Constraints, [Type], [ProgEq])]
es <- [ProgEq] -> State Env [(Subst, Constraints, [Type], [ProgEq])]
inferLetEqs [ProgEq]
eqs
            [[(Subst, Constraints, Type, Term)]]
rs <- ((Subst, Constraints, [Type], [ProgEq])
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, [Type], [ProgEq])]
-> State Env [[(Subst, Constraints, Type, Term)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (s1 :: Subst
s1, cs :: Constraints
cs, _, nes :: [ProgEq]
nes) -> do
               (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (ProgEq -> [VarDecl]) -> [ProgEq] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                         ( \ (ProgEq p :: Term
p _ _) -> Term -> [VarDecl]
extractVars Term
p) [ProgEq]
nes
               [(Subst, Constraints, Type, Term)]
ts <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
False Term
inTrm
               [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s2 :: Subst
s2, cr :: Constraints
cr, ty :: Type
ty, nt :: Term
nt) ->
                              (Subst -> Subst -> Subst
compSubst Subst
s1 Subst
s2,
                               Subst -> Constraints -> Constraints
substC Subst
s2 Constraints
cs Constraints -> Constraints -> Constraints
`joinC` Constraints
cr,
                               Type
ty, LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
br [ProgEq]
nes Term
nt Range
ps)) [(Subst, Constraints, Type, Term)]
ts) [(Subst, Constraints, [Type], [ProgEq])]
es
            Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
            [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Term)]]
-> [(Subst, Constraints, Type, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Term)]]
rs
        AsPattern (VarDecl v :: Id
v _ ok :: SeparatorKind
ok qs :: Range
qs) pat :: Term
pat ps :: Range
ps -> do
           [(Subst, Constraints, Type, Term)]
pats <- Bool -> Term -> State Env [(Subst, Constraints, Type, Term)]
infer Bool
True Term
pat
           [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Term)]
 -> State Env [(Subst, Constraints, Type, Term)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Term))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s1 :: Subst
s1, cs :: Constraints
cs, t1 :: Type
t1, p1 :: Term
p1) -> (Subst
s1, Constraints
cs, Type
t1,
                          VarDecl -> Term -> Range -> Term
AsPattern (Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v Type
t1 SeparatorKind
ok Range
qs) Term
p1 Range
ps)) [(Subst, Constraints, Type, Term)]
pats
        _ -> do Type
ty <- Term -> State Env Type
freshTypeVar Term
trm
                [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> [Char] -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Error "unexpected term" Term
trm]
                [(Subst, Constraints, Type, Term)]
-> State Env [(Subst, Constraints, Type, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst
eps, Constraints
noC, Type
ty, Term
trm)]

inferLetEqs :: [ProgEq] -> State Env [(Subst, Constraints, [Type], [ProgEq])]
inferLetEqs :: [ProgEq] -> State Env [(Subst, Constraints, [Type], [ProgEq])]
inferLetEqs es :: [ProgEq]
es = do
    let pats :: [Term]
pats = (ProgEq -> Term) -> [ProgEq] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ProgEq p :: Term
p _ _) -> Term
p) [ProgEq]
es
        trms :: [Term]
trms = (ProgEq -> Term) -> [ProgEq] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ProgEq _ t :: Term
t _) -> Term
t) [ProgEq]
es
        qs :: [Range]
qs = (ProgEq -> Range) -> [ProgEq] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ProgEq _ _ q :: Range
q) -> Range
q) [ProgEq]
es
    do Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
       [(Subst, Constraints, [Type], [Term])]
newPats <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
True ((Term -> Maybe Type) -> [Term] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Type -> Term -> Maybe Type
forall a b. a -> b -> a
const Maybe Type
forall a. Maybe a
Nothing) [Term]
pats) [Term]
pats
       [[(Subst, Constraints, [Type], [ProgEq])]]
combs <- ((Subst, Constraints, [Type], [Term])
 -> State Env [(Subst, Constraints, [Type], [ProgEq])])
-> [(Subst, Constraints, [Type], [Term])]
-> State Env [[(Subst, Constraints, [Type], [ProgEq])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (sf :: Subst
sf, pcs :: Constraints
pcs, tys :: [Type]
tys, pps :: [Term]
pps) -> do
             (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
pps
             [(Subst, Constraints, [Type], [Term])]
newTrms <- Bool
-> [Maybe Type]
-> [Term]
-> State Env [(Subst, Constraints, [Type], [Term])]
checkList Bool
False ((Type -> Maybe Type) -> [Type] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Maybe Type
forall a. a -> Maybe a
Just [Type]
tys) [Term]
trms
             [(Subst, Constraints, [Type], [ProgEq])]
-> State Env [(Subst, Constraints, [Type], [ProgEq])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, [Type], [ProgEq])]
 -> State Env [(Subst, Constraints, [Type], [ProgEq])])
-> [(Subst, Constraints, [Type], [ProgEq])]
-> State Env [(Subst, Constraints, [Type], [ProgEq])]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, [Type], [Term])
 -> (Subst, Constraints, [Type], [ProgEq]))
-> [(Subst, Constraints, [Type], [Term])]
-> [(Subst, Constraints, [Type], [ProgEq])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (sr :: Subst
sr, tcs :: Constraints
tcs, tys2 :: [Type]
tys2, tts :: [Term]
tts ) ->
                          (Subst -> Subst -> Subst
compSubst Subst
sf Subst
sr,
                           Constraints -> Constraints -> Constraints
joinC Constraints
tcs (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ Subst -> Constraints -> Constraints
substC Subst
sr Constraints
pcs, [Type]
tys2,
                           (Term -> Term -> Range -> ProgEq)
-> [Term] -> [Term] -> [Range] -> [ProgEq]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (Term -> Term -> Range -> ProgEq
ProgEq (Term -> Term -> Range -> ProgEq)
-> (Term -> Term) -> Term -> Term -> Range -> ProgEq
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Term -> Term
substTerm Subst
sr)
                               [Term]
pps [Term]
tts [Range]
qs)) [(Subst, Constraints, [Type], [Term])]
newTrms) [(Subst, Constraints, [Type], [Term])]
newPats
       Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
       [(Subst, Constraints, [Type], [ProgEq])]
-> State Env [(Subst, Constraints, [Type], [ProgEq])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, [Type], [ProgEq])]
 -> State Env [(Subst, Constraints, [Type], [ProgEq])])
-> [(Subst, Constraints, [Type], [ProgEq])]
-> State Env [(Subst, Constraints, [Type], [ProgEq])]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, [Type], [ProgEq])]]
-> [(Subst, Constraints, [Type], [ProgEq])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, [Type], [ProgEq])]]
combs

inferCaseEq :: Type -> Type -> ProgEq
            -> State Env [(Subst, Constraints, Type, Type, ProgEq)]
inferCaseEq :: Type
-> Type
-> ProgEq
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
inferCaseEq pty :: Type
pty tty :: Type
tty (ProgEq pat :: Term
pat trm :: Term
trm ps :: Range
ps) = do
   [(Subst, Constraints, Type, Term)]
pats1 <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
True (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
pty) Term
pat
   Env
e <- State Env Env
forall s. State s s
get
   let pats :: [(Subst, Constraints, Type, Term)]
pats = ((Subst, Constraints, Type, Term) -> Bool)
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (_, _, _, p :: Term
p) -> Env -> Term -> Bool
isPat Env
e Term
p) [(Subst, Constraints, Type, Term)]
pats1
       ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
e
   Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Subst, Constraints, Type, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Subst, Constraints, Type, Term)]
pats)
     (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> [Char] -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Hint "unresolved case pattern" Term
pat]
   Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
   [[(Subst, Constraints, Type, Type, ProgEq)]]
es <- ((Subst, Constraints, Type, Term)
 -> State Env [(Subst, Constraints, Type, Type, ProgEq)])
-> [(Subst, Constraints, Type, Term)]
-> State Env [[(Subst, Constraints, Type, Type, ProgEq)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ (s :: Subst
s, cs :: Constraints
cs, ty :: Type
ty, p :: Term
p) -> do
                (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
p
                [(Subst, Constraints, Type, Term)]
ts <- Bool
-> Maybe Type
-> Term
-> State Env [(Subst, Constraints, Type, Term)]
inferWithMaybeType Bool
False (Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
subst Subst
s Type
tty) Term
trm
                Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
                [(Subst, Constraints, Type, Type, ProgEq)]
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Type, ProgEq)]
 -> State Env [(Subst, Constraints, Type, Type, ProgEq)])
-> [(Subst, Constraints, Type, Type, ProgEq)]
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Term)
 -> (Subst, Constraints, Type, Type, ProgEq))
-> [(Subst, Constraints, Type, Term)]
-> [(Subst, Constraints, Type, Type, ProgEq)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (st :: Subst
st, cr :: Constraints
cr, tyt :: Type
tyt, t :: Term
t) ->
                       (Subst -> Subst -> Subst
compSubst Subst
s Subst
st,
                        Subst -> Constraints -> Constraints
substC Subst
st Constraints
cs Constraints -> Constraints -> Constraints
`joinC` Constraints
cr,
                        Subst -> Type -> Type
subst Subst
st Type
ty, Type
tyt,
                        Term -> Term -> Range -> ProgEq
ProgEq Term
p Term
t Range
ps)) [(Subst, Constraints, Type, Term)]
ts) [(Subst, Constraints, Type, Term)]
pats
   [(Subst, Constraints, Type, Type, ProgEq)]
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Type, ProgEq)]
 -> State Env [(Subst, Constraints, Type, Type, ProgEq)])
-> [(Subst, Constraints, Type, Type, ProgEq)]
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Type, ProgEq)]]
-> [(Subst, Constraints, Type, Type, ProgEq)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Type, ProgEq)]]
es

inferCaseEqs :: Type -> Type -> [ProgEq]
            -> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
inferCaseEqs :: Type
-> Type
-> [ProgEq]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
inferCaseEqs pty :: Type
pty tTy :: Type
tTy [] = [(Subst, Constraints, Type, Type, [ProgEq])]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Subst
eps, Constraints
noC, Type
pty, Type
tTy, [])]
inferCaseEqs pty :: Type
pty tty :: Type
tty (eq :: ProgEq
eq : eqs :: [ProgEq]
eqs) = do
  [(Subst, Constraints, Type, Type, ProgEq)]
fts <- Type
-> Type
-> ProgEq
-> State Env [(Subst, Constraints, Type, Type, ProgEq)]
inferCaseEq Type
pty Type
tty ProgEq
eq
  [[(Subst, Constraints, Type, Type, [ProgEq])]]
rs <- ((Subst, Constraints, Type, Type, ProgEq)
 -> State Env [(Subst, Constraints, Type, Type, [ProgEq])])
-> [(Subst, Constraints, Type, Type, ProgEq)]
-> State Env [[(Subst, Constraints, Type, Type, [ProgEq])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (s :: Subst
s, cs :: Constraints
cs, pty1 :: Type
pty1, tty1 :: Type
tty1, ne :: ProgEq
ne) -> do
              [(Subst, Constraints, Type, Type, [ProgEq])]
rts <- Type
-> Type
-> [ProgEq]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
inferCaseEqs Type
pty1 Type
tty1 [ProgEq]
eqs
              [(Subst, Constraints, Type, Type, [ProgEq])]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Type, [ProgEq])]
 -> State Env [(Subst, Constraints, Type, Type, [ProgEq])])
-> [(Subst, Constraints, Type, Type, [ProgEq])]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
forall a b. (a -> b) -> a -> b
$ ((Subst, Constraints, Type, Type, [ProgEq])
 -> (Subst, Constraints, Type, Type, [ProgEq]))
-> [(Subst, Constraints, Type, Type, [ProgEq])]
-> [(Subst, Constraints, Type, Type, [ProgEq])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s2 :: Subst
s2, cr :: Constraints
cr, pty2 :: Type
pty2, tty2 :: Type
tty2, nes :: [ProgEq]
nes) ->
                             (Subst -> Subst -> Subst
compSubst Subst
s Subst
s2,
                              Subst -> Constraints -> Constraints
substC Subst
s2 Constraints
cs Constraints -> Constraints -> Constraints
`joinC` Constraints
cr,
                              Type
pty2, Type
tty2, ProgEq
ne ProgEq -> [ProgEq] -> [ProgEq]
forall a. a -> [a] -> [a]
: [ProgEq]
nes)) [(Subst, Constraints, Type, Type, [ProgEq])]
rts) [(Subst, Constraints, Type, Type, ProgEq)]
fts
  [(Subst, Constraints, Type, Type, [ProgEq])]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Subst, Constraints, Type, Type, [ProgEq])]
 -> State Env [(Subst, Constraints, Type, Type, [ProgEq])])
-> [(Subst, Constraints, Type, Type, [ProgEq])]
-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
forall a b. (a -> b) -> a -> b
$ [[(Subst, Constraints, Type, Type, [ProgEq])]]
-> [(Subst, Constraints, Type, Type, [ProgEq])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Subst, Constraints, Type, Type, [ProgEq])]]
rs