-- |
-- Module      :  Cryptol.TypeCheck.Infer
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Assumes that the `NoPat` pass has been run.

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant <$>" #-}
{-# HLINT ignore "Redundant <&>" #-}
module Cryptol.TypeCheck.Infer
  ( checkE
  , checkSigB
  , inferTopModule
  , inferBinds
  , checkTopDecls
  )
where

import Data.Text(Text)
import qualified Data.Text as Text


import           Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc, nameIdent)
import           Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.ModuleSystem.Exports as P
import           Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
import           Cryptol.TypeCheck.Monad
import           Cryptol.TypeCheck.Error
import           Cryptol.TypeCheck.Solve
import           Cryptol.TypeCheck.SimpType(tMul)
import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
                                        checkPropSyn,checkNewtype,checkEnum,
                                        checkParameterType,
                                        checkPrimType,
                                        checkParameterConstraints,
                                        checkPropGuards)
import           Cryptol.TypeCheck.Instantiate
import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import           Cryptol.TypeCheck.Unify(rootPath)
import           Cryptol.TypeCheck.Module
import           Cryptol.TypeCheck.FFI
import           Cryptol.TypeCheck.FFI.FFIType
import           Cryptol.Utils.Ident
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.RecordMap
import           Cryptol.IR.TraverseNames(mapNames)
import           Cryptol.Utils.PP (pp)

import qualified Data.Map as Map
import           Data.Map (Map)
import qualified Data.Set as Set
import           Data.List(foldl', sortBy, groupBy, partition)
import           Data.Either(partitionEithers)
import           Data.Maybe(isJust, fromMaybe, mapMaybe)
import           Data.Ratio(numerator,denominator)
import           Data.Traversable(forM)
import           Data.Function(on)
import           Control.Monad(zipWithM, unless, foldM, forM_, mplus, zipWithM,
                               unless, foldM, forM_, mplus, when)

-- import Debug.Trace
-- import Cryptol.TypeCheck.PP

inferTopModule :: P.Module Name -> InferM TCTopEntity
inferTopModule :: Module Name -> InferM TCTopEntity
inferTopModule Module Name
m =
  case Module Name -> ModuleDefinition Name
forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef Module Name
m of
    P.NormalModule [TopDecl Name]
ds ->
      do ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope (Located ModName -> ModName
forall a. Located a -> a
thing (Module Name -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m)) ([TopDecl Name] -> ExportSpec Name
forall name. Ord name => [TopDecl name] -> ExportSpec name
P.exportedDecls [TopDecl Name]
ds) (Module Name -> NamingEnv
forall mname name. ModuleG mname name -> NamingEnv
P.mInScope Module Name
m)
         [TopDecl Name] -> InferM ()
checkTopDecls [TopDecl Name]
ds
         InferM ()
proveModuleTopLevel
         InferM TCTopEntity
endModule

    P.FunctorInstance Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst ->
      do Maybe TCTopEntity
mb <- Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> ModuleInstance Name
-> NamingEnv
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst
           (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop (ModName -> ImpName Name)
-> Located ModName -> Located (ImpName Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Module Name -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m) Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst (Module Name -> NamingEnv
forall mname name. ModuleG mname name -> NamingEnv
P.mInScope Module Name
m) Maybe Text
forall a. Maybe a
Nothing
         case Maybe TCTopEntity
mb of
           Just TCTopEntity
mo -> TCTopEntity -> InferM TCTopEntity
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCTopEntity
mo
           Maybe TCTopEntity
Nothing -> String -> [String] -> InferM TCTopEntity
forall a. HasCallStack => String -> [String] -> a
panic String
"inferModule" [String
"Didnt' get a module"]

    P.InterfaceModule Signature Name
sig ->
      do ModName -> InferM ()
newTopSignatureScope (Located ModName -> ModName
forall a. Located a -> a
thing (Module Name -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module Name
m))
         Signature Name -> InferM ()
checkSignature Signature Name
sig
         InferM TCTopEntity
endTopSignature




-- | Construct a Prelude primitive in the parsed AST.
mkPrim :: String -> InferM (P.Expr Name)
mkPrim :: String -> InferM (Expr Name)
mkPrim String
str =
  do Name
nm <- String -> InferM Name
mkPrim' String
str
     Expr Name -> InferM (Expr Name)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
nm)

-- | Construct a Prelude primitive in the parsed AST.
mkPrim' :: String -> InferM Name
mkPrim' :: String -> InferM Name
mkPrim' String
str =
  do PrimMap
prims <- InferM PrimMap
getPrimMap
     Name -> InferM Name
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimIdent -> PrimMap -> Name
lookupPrimDecl (Text -> PrimIdent
prelPrim (String -> Text
Text.pack String
str)) PrimMap
prims)



desugarLiteral :: P.Literal -> InferM (P.Expr Name)
desugarLiteral :: Literal -> InferM (Expr Name)
desugarLiteral Literal
lit =
  do Range
l <- InferM Range
curRange
     Expr Name
numberPrim <- String -> InferM (Expr Name)
mkPrim String
"number"
     Expr Name
fracPrim   <- String -> InferM (Expr Name)
mkPrim String
"fraction"
     let named :: (String, Type name) -> TypeInst name
named (String
x,Type name
y)  = Named (Type name) -> TypeInst name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
                        P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type name
value = Type name
y }
         number :: [(String, Type Name)] -> Expr Name
number [(String, Type Name)]
fs    = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
numberPrim (((String, Type Name) -> TypeInst Name)
-> [(String, Type Name)] -> [TypeInst Name]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type Name) -> TypeInst Name
forall {name}. (String, Type name) -> TypeInst name
named [(String, Type Name)]
fs)
         tBits :: Integer -> Type n
tBits Integer
n = Type n -> Type n -> Type n
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type n
forall n. Integer -> Type n
P.TNum Integer
n) Type n
forall n. Type n
P.TBit

     Expr Name -> InferM (Expr Name)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name -> InferM (Expr Name))
-> Expr Name -> InferM (Expr Name)
forall a b. (a -> b) -> a -> b
$ case Literal
lit of

       P.ECNum Integer
num NumInfo
info ->
         [(String, Type Name)] -> Expr Name
number ([(String, Type Name)] -> Expr Name)
-> [(String, Type Name)] -> Expr Name
forall a b. (a -> b) -> a -> b
$ [ (String
"val", Integer -> Type Name
forall n. Integer -> Type n
P.TNum Integer
num) ] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++ case NumInfo
info of
           P.BinLit Text
_ Int
n  -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
           P.OctLit Text
_ Int
n  -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
           P.HexLit Text
_ Int
n  -> [ (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
4 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)) ]
           P.DecLit Text
_    -> [ ]
           P.PolyLit Int
_n  -> [ (String
"rep", Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild Type Name
forall n. Type n
P.TBit) ]

       P.ECFrac Rational
fr FracInfo
info ->
         let arg :: (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
f = Type name -> TypeInst name
forall name. Type name -> TypeInst name
P.PosInst (Integer -> Type name
forall n. Integer -> Type n
P.TNum (Rational -> Integer
f Rational
fr))
             rnd :: TypeInst name
rnd   = Type name -> TypeInst name
forall name. Type name -> TypeInst name
P.PosInst (Integer -> Type name
forall n. Integer -> Type n
P.TNum (case FracInfo
info of
                                          P.DecFrac Text
_ -> Integer
0
                                          P.BinFrac Text
_ -> Integer
1
                                          P.OctFrac Text
_ -> Integer
1
                                          P.HexFrac Text
_ -> Integer
1))
         in Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
fracPrim [ (Rational -> Integer) -> TypeInst Name
forall {name}. (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
forall a. Ratio a -> a
numerator, (Rational -> Integer) -> TypeInst Name
forall {name}. (Rational -> Integer) -> TypeInst name
arg Rational -> Integer
forall a. Ratio a -> a
denominator, TypeInst Name
forall {name}. TypeInst name
rnd ]

       P.ECChar Char
c ->
         [(String, Type Name)] -> Expr Name
number [ (String
"val", Integer -> Type Name
forall n. Integer -> Type n
P.TNum (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c)))
                , (String
"rep", Integer -> Type Name
forall n. Integer -> Type n
tBits (Integer
8 :: Integer)) ]

       P.ECString String
s ->
          Expr Name -> Type Name -> Expr Name
forall n. Expr n -> Type n -> Expr n
P.ETyped ([Expr Name] -> Expr Name
forall n. [Expr n] -> Expr n
P.EList [ Literal -> Expr Name
forall n. Literal -> Expr n
P.ELit (Char -> Literal
P.ECChar Char
c) | Char
c <- String
s ])
                   (Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq Type Name
forall n. Type n
P.TWild (Type Name -> Type Name -> Type Name
forall n. Type n -> Type n -> Type n
P.TSeq (Integer -> Type Name
forall n. Integer -> Type n
P.TNum Integer
8) Type Name
forall n. Type n
P.TBit))



-- | Infer the type of an expression with an explicit instantiation.
appTys :: P.Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys :: Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
expr [TypeArg]
ts TypeWithSource
tGoal =
  case Expr Name
expr of
    P.EVar Name
x ->
      do VarType
res <- Name -> InferM VarType
lookupVar Name
x
         (Expr
e',Prop
t) <- case VarType
res of
           ExtVar Schema
s   -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s [TypeArg]
ts
           CurSCC Expr
e Prop
t -> do [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
                            (Expr, Prop) -> InferM (Expr, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e,Prop
t)

         Prop -> TypeWithSource -> InferM ()
checkHasType Prop
t TypeWithSource
tGoal
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'

    P.ELit Literal
l -> do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
                   Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal


    P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [TypeArg]
ts) TypeWithSource
tGoal

    -- Here is an example of why this might be useful:
    -- f ` { x = T } where type T = ...
    P.EWhere Expr Name
e [Decl Name]
ds ->
      do (Expr
e1,[DeclGroup]
ds1) <- [Decl Name] -> InferM Expr -> InferM (Expr, [DeclGroup])
forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
         Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)

    P.ELocated Expr Name
e Range
r ->
      do Expr
e' <- Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal)
         Bool
cs <- InferM Bool
getCallStacks
         if Bool
cs then Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'

    P.EGenerate   {} -> InferM Expr
mono

    P.ETuple    {} -> InferM Expr
mono
    P.ERecord   {} -> InferM Expr
mono
    P.EUpd      {} -> InferM Expr
mono
    P.ESel      {} -> InferM Expr
mono
    P.EList     {} -> InferM Expr
mono
    P.EFromTo   {} -> InferM Expr
mono
    P.EFromToBy {} -> InferM Expr
mono
    P.EFromToDownBy {} -> InferM Expr
mono
    P.EFromToLessThan {} -> InferM Expr
mono
    P.EInfFrom  {} -> InferM Expr
mono
    P.EComp     {} -> InferM Expr
mono
    P.EApp      {} -> InferM Expr
mono
    P.EIf       {} -> InferM Expr
mono
    P.ETyped    {} -> InferM Expr
mono
    P.ETypeVal  {} -> InferM Expr
mono
    P.EFun      {} -> InferM Expr
mono
    P.ESplit    {} -> InferM Expr
mono
    P.EPrefix   {} -> InferM Expr
mono
    P.ECase {}     -> InferM Expr
mono

    P.EParens Expr Name
e       -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg]
ts TypeWithSource
tGoal
    P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) [TypeArg]
ts TypeWithSource
tGoal

  where mono :: InferM Expr
mono = do Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal
                  [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts
                  Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'

checkNoParams :: [TypeArg] -> InferM ()
checkNoParams :: [TypeArg] -> InferM ()
checkNoParams [TypeArg]
ts =
  case [TypeArg]
pos of
    TypeArg
p : [TypeArg]
_ -> do Range
r <- case TypeArg -> MaybeCheckedType
tyArgType TypeArg
p of
                       Unchecked Type Name
t | Just Range
r <- Type Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t -> Range -> InferM Range
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Range
r
                       MaybeCheckedType
_ -> InferM Range
curRange
                Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
r (Error -> InferM ()
recordError Error
TooManyPositionalTypeParams)
    [TypeArg]
_ -> (TypeArg -> InferM ()) -> [TypeArg] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TypeArg -> InferM ()
badNamed [TypeArg]
named
  where
  badNamed :: TypeArg -> InferM ()
badNamed TypeArg
l =
    case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
l of
      Just Located Ident
i  -> Error -> InferM ()
recordError (Located Ident -> Error
UndefinedTypeParameter Located Ident
i)
      Maybe (Located Ident)
Nothing -> () -> InferM ()
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  ([TypeArg]
named,[TypeArg]
pos) = (TypeArg -> Bool) -> [TypeArg] -> ([TypeArg], [TypeArg])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Located Ident) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Located Ident) -> Bool)
-> (TypeArg -> Maybe (Located Ident)) -> TypeArg -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeArg -> Maybe (Located Ident)
tyArgName) [TypeArg]
ts


checkTypeOfKind :: P.Type Name -> Kind -> InferM Type
checkTypeOfKind :: Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
ty Kind
k = Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
ty (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
k)


-- | Infer the type of an expression, and translate it to a fully elaborated
-- core term.
checkE :: P.Expr Name -> TypeWithSource -> InferM Expr
checkE :: Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
expr TypeWithSource
tGoal =
  case Expr Name
expr of
    P.EVar Name
x ->
      do VarType
res <- Name -> InferM VarType
lookupVar Name
x
         (Expr
e',Prop
t) <- case VarType
res of
                     ExtVar Schema
s   -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
x (Name -> Expr
EVar Name
x) Schema
s []
                     CurSCC Expr
e Prop
t -> (Expr, Prop) -> InferM (Expr, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Prop
t)

         Prop -> TypeWithSource -> InferM ()
checkHasType Prop
t TypeWithSource
tGoal
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'

    P.EGenerate Expr Name
e ->
      do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"generate"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal

    P.ELit l :: Literal
l@(P.ECNum Integer
_ (P.DecLit Text
_)) ->
      do Expr Name
e <- Literal -> InferM (Expr Name)
desugarLiteral Literal
l
         -- NOTE: When 'l' is a decimal literal, 'desugarLiteral' does
         -- not generate an instantiation for the 'rep' type argument
         -- of the 'number' primitive. Therefore we explicitly
         -- instantiate 'rep' to 'tGoal' in this case to avoid
         -- generating an unnecessary unification variable.
         Range
loc <- InferM Range
curRange
         let arg :: TypeArg
arg = TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = Located Ident -> Maybe (Located Ident)
forall a. a -> Maybe a
Just (Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
loc (String -> Ident
packIdent String
"rep"))
                           , tyArgType :: MaybeCheckedType
tyArgType = Prop -> MaybeCheckedType
Checked (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
                           }
         Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e [TypeArg
arg] TypeWithSource
tGoal

    P.ELit Literal
l -> (Expr Name -> TypeWithSource -> InferM Expr
`checkE` TypeWithSource
tGoal) (Expr Name -> InferM Expr) -> InferM (Expr Name) -> InferM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Literal -> InferM (Expr Name)
desugarLiteral Literal
l

    P.ETuple [Expr Name]
es ->
      do [Prop]
etys <- Int -> TypeWithSource -> InferM [Prop]
expectTuple ([Expr Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) TypeWithSource
tGoal
         let mkTGoal :: Int -> Prop -> t -> TypeWithSource
mkTGoal Int
n Prop
t t
e = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Int -> TypeSource
TypeOfTupleField Int
n) (t -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc t
e)
         [Expr]
es'  <- (Expr Name -> TypeWithSource -> InferM Expr)
-> [Expr Name] -> [TypeWithSource] -> InferM [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Name -> TypeWithSource -> InferM Expr
checkE [Expr Name]
es ((Int -> Prop -> Expr Name -> TypeWithSource)
-> [Int] -> [Prop] -> [Expr Name] -> [TypeWithSource]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> Prop -> Expr Name -> TypeWithSource
forall {t}. HasLoc t => Int -> Prop -> t -> TypeWithSource
mkTGoal [Int
1..] [Prop]
etys [Expr Name]
es)
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Expr
ETuple [Expr]
es')

    P.ERecord Rec (Expr Name)
fs ->
      do RecordMap Ident (Expr Name, Prop)
es  <- Rec (Expr Name)
-> TypeWithSource -> InferM (RecordMap Ident (Expr Name, Prop))
forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec Rec (Expr Name)
fs TypeWithSource
tGoal
         let checkField :: Ident -> (Expr Name, Prop) -> InferM Expr
checkField Ident
f (Expr Name
e,Prop
t) =
                Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Ident -> TypeSource
TypeOfRecordField Ident
f) (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
         RecordMap Ident Expr
es' <- (Ident -> (Expr Name, Prop) -> InferM Expr)
-> RecordMap Ident (Expr Name, Prop)
-> InferM (RecordMap Ident Expr)
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap Ident -> (Expr Name, Prop) -> InferM Expr
checkField RecordMap Ident (Expr Name, Prop)
es
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
es')

    P.EUpd Maybe (Expr Name)
x [UpdField Name]
fs -> Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
x [UpdField Name]
fs TypeWithSource
tGoal

    P.ESel Expr Name
e Selector
l ->
      do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
l
         Prop
t <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
         Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t TypeSource
src (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
         HasGoalSln
f <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
l Prop
t (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
f Expr
e')

    P.EList [] ->
      do (Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal
         Int -> TypeWithSource -> InferM ()
expectFin Int
0 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [] Prop
a)

    P.EList [Expr Name]
es ->
      do (Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal
         Int -> TypeWithSource -> InferM ()
expectFin ([Expr Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Name]
es) (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
         let checkElem :: Expr Name -> InferM Expr
checkElem Expr Name
e = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
a TypeSource
TypeOfSeqElement (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
         [Expr]
es' <- (Expr Name -> InferM Expr) -> [Expr Name] -> InferM [Expr]
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 Expr Name -> InferM Expr
checkElem [Expr Name]
es
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> Prop -> Expr
EList [Expr]
es' Prop
a)

    P.EFromToBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
      | Bool
isStrict ->
        do Range
l <- InferM Range
curRange
           let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
                    case Maybe (Type Name)
mety of
                      Just Type Name
ety -> [(String
"a",Type Name
ety)]
                      Maybe (Type Name)
Nothing  -> []
           Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToByLessThan"
           let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                    [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                    | (String
x,Type Name
y) <- [(String, Type Name)]
fs
                    ]
           Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
      | Bool
otherwise ->
        do Range
l <- InferM Range
curRange
           let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
                    case Maybe (Type Name)
mety of
                      Just Type Name
ety -> [(String
"a",Type Name
ety)]
                      Maybe (Type Name)
Nothing  -> []
           Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToBy"
           let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                    [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                    | (String
x,Type Name
y) <- [(String, Type Name)]
fs
                    ]
           Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal

    P.EFromToDownBy Bool
isStrict Type Name
t1 Type Name
t2 Type Name
t3 Maybe (Type Name)
mety
      | Bool
isStrict ->
        do Range
l <- InferM Range
curRange
           let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"bound",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
                    case Maybe (Type Name)
mety of
                      Just Type Name
ety -> [(String
"a",Type Name
ety)]
                      Maybe (Type Name)
Nothing  -> []
           Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownByGreaterThan"
           let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                    [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                    | (String
x,Type Name
y) <- [(String, Type Name)]
fs
                    ]
           Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal
      | Bool
otherwise ->
        do Range
l <- InferM Range
curRange
           let fs :: [(String, Type Name)]
fs = [(String
"first",Type Name
t1),(String
"last",Type Name
t2),(String
"stride",Type Name
t3)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++
                    case Maybe (Type Name)
mety of
                      Just Type Name
ety -> [(String
"a",Type Name
ety)]
                      Maybe (Type Name)
Nothing  -> []
           Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToDownBy"
           let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                    [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named{ name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                    | (String
x,Type Name
y) <- [(String, Type Name)]
fs
                    ]
           Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal

    P.EFromToLessThan Type Name
t1 Type Name
t2 Maybe (Type Name)
mety ->
      do Range
l <- InferM Range
curRange
         let fs0 :: [(String, Type Name)]
fs0 =
               case Maybe (Type Name)
mety of
                 Just Type Name
ety -> [(String
"a", Type Name
ety)]
                 Maybe (Type Name)
Nothing  -> []
         let fs :: [(String, Type Name)]
fs = [(String
"first", Type Name
t1), (String
"bound", Type Name
t2)] [(String, Type Name)]
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. [a] -> [a] -> [a]
++ [(String, Type Name)]
fs0
         Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"fromToLessThan"
         let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                  [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                  | (String
x,Type Name
y) <- [(String, Type Name)]
fs
                  ]
         Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal

    P.EFromTo Type Name
t1 Maybe (Type Name)
mbt2 Type Name
t3 Maybe (Type Name)
mety ->
      do Range
l <- InferM Range
curRange
         let fs0 :: [(String, Type Name)]
fs0 =
               case Maybe (Type Name)
mety of
                 Just Type Name
ety -> [(String
"a", Type Name
ety)]
                 Maybe (Type Name)
Nothing -> []
         let (String
c,[(String, Type Name)]
fs) =
               case Maybe (Type Name)
mbt2 of
                 Maybe (Type Name)
Nothing ->
                    (String
"fromTo", (String
"last", Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)
                 Just Type Name
t2 ->
                    (String
"fromThenTo", (String
"next",Type Name
t2) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: (String
"last",Type Name
t3) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs0)

         Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
c
         let e' :: Expr Name
e' = Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                  [ Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
x), value :: Type Name
value = Type Name
y }
                  | (String
x,Type Name
y) <- (String
"first",Type Name
t1) (String, Type Name)
-> [(String, Type Name)] -> [(String, Type Name)]
forall a. a -> [a] -> [a]
: [(String, Type Name)]
fs
                  ]

         Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e' TypeWithSource
tGoal

    P.EInfFrom Expr Name
e1 Maybe (Expr Name)
Nothing ->
      do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFrom"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) TypeWithSource
tGoal

    P.EInfFrom Expr Name
e1 (Just Expr Name
e2) ->
      do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"infFromThen"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e1) Expr Name
e2) TypeWithSource
tGoal

    P.EComp Expr Name
e [[Match Name]]
mss ->
      do ([[Match]]
mss', [Map Name (Located Prop)]
dss, [Prop]
ts) <- [([Match], Map Name (Located Prop), Prop)]
-> ([[Match]], [Map Name (Located Prop)], [Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([Match], Map Name (Located Prop), Prop)]
 -> ([[Match]], [Map Name (Located Prop)], [Prop]))
-> InferM [([Match], Map Name (Located Prop), Prop)]
-> InferM ([[Match]], [Map Name (Located Prop)], [Prop])
forall a b. (a -> b) -> InferM a -> InferM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int
 -> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop))
-> [Int]
-> [[Match Name]]
-> InferM [([Match], Map Name (Located Prop), Prop)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm [ Int
1 .. ] [[Match Name]]
mss
         (Prop
len,Prop
a) <- TypeWithSource -> InferM (Prop, Prop)
expectSeq TypeWithSource
tGoal

         Prop
inferred <- [Prop] -> InferM Prop
smallest [Prop]
ts
         [Prop]
ctrs <- TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
len TypeSource
LenOfSeq (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr)) Prop
inferred
         ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [Prop]
ctrs

         Map Name (Located Prop)
ds     <- [Map Name (Located Prop)] -> InferM (Map Name (Located Prop))
forall {m :: * -> *} {k} {a}.
(Monad m, Show k, Ord k) =>
[Map k (Located a)] -> m (Map k (Located a))
combineMaps [Map Name (Located Prop)]
dss
         Expr
e'     <- Map Name (Located Prop) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e
                                (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
a TypeSource
TypeOfSeqElement (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e)))
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp Prop
len Prop
a Expr
e' [[Match]]
mss')
      where
      -- the renamer should have made these checks already?
      combineMaps :: [Map k (Located a)] -> m (Map k (Located a))
combineMaps [Map k (Located a)]
ms = if [(k, [Range])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(k, [Range])]
bad
                          then Map k (Located a) -> m (Map k (Located a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Map k (Located a)] -> Map k (Located a)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map k (Located a)]
ms)
                          else String -> [String] -> m (Map k (Located a))
forall a. HasCallStack => String -> [String] -> a
panic String
"combineMaps" ([String] -> m (Map k (Located a)))
-> [String] -> m (Map k (Located a))
forall a b. (a -> b) -> a -> b
$ String
"Multiple definitions"
                                                      String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((k, [Range]) -> String) -> [(k, [Range])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (k, [Range]) -> String
forall a. Show a => a -> String
show [(k, [Range])]
bad
          where
          bad :: [(k, [Range])]
bad = do Map k (Located a)
m <- [Map k (Located a)]
ms
                   [Located k] -> [(k, [Range])]
duplicates [ Located a
a { thing = x } | (k
x,Located a
a) <- Map k (Located a) -> [(k, Located a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k (Located a)
m ]
          duplicates :: [Located k] -> [(k, [Range])]
duplicates = ([Located k] -> Maybe (k, [Range]))
-> [[Located k]] -> [(k, [Range])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Located k] -> Maybe (k, [Range])
forall {a}. [Located a] -> Maybe (a, [Range])
multiple
                     ([[Located k]] -> [(k, [Range])])
-> ([Located k] -> [[Located k]]) -> [Located k] -> [(k, [Range])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located k -> Located k -> Bool) -> [Located k] -> [[Located k]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (k -> k -> Bool
forall a. Eq a => a -> a -> Bool
(==) (k -> k -> Bool)
-> (Located k -> k) -> Located k -> Located k -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located k -> k
forall a. Located a -> a
thing)
                     ([Located k] -> [[Located k]])
-> ([Located k] -> [Located k]) -> [Located k] -> [[Located k]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located k -> Located k -> Ordering) -> [Located k] -> [Located k]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (k -> k -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (k -> k -> Ordering)
-> (Located k -> k) -> Located k -> Located k -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Located k -> k
forall a. Located a -> a
thing)
            where
            multiple :: [Located a] -> Maybe (a, [Range])
multiple xs :: [Located a]
xs@(Located a
x : Located a
_ : [Located a]
_) = (a, [Range]) -> Maybe (a, [Range])
forall a. a -> Maybe a
Just (Located a -> a
forall a. Located a -> a
thing Located a
x, (Located a -> Range) -> [Located a] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Located a -> Range
forall a. Located a -> Range
srcRange [Located a]
xs)
            multiple [Located a]
_              = Maybe (a, [Range])
forall a. Maybe a
Nothing



    P.EAppT Expr Name
e [TypeInst Name]
fs -> Expr Name -> [TypeArg] -> TypeWithSource -> InferM Expr
appTys Expr Name
e ((TypeInst Name -> TypeArg) -> [TypeInst Name] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> TypeArg
uncheckedTypeArg [TypeInst Name]
fs) TypeWithSource
tGoal

    P.EApp Expr Name
e1 Expr Name
e2 ->
      do let argSrc :: TypeSource
argSrc = ArgDescr -> TypeSource
TypeOfArg ArgDescr
noArgDescr
         Prop
t1  <- TypeSource -> Kind -> InferM Prop
newType TypeSource
argSrc  Kind
KType
         Expr
e1' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1
                  (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tFun Prop
t1 (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)) TypeSource
FunApp (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e1))
         Expr
e2' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t1 TypeSource
argSrc (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e2))
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')

    P.EIf Expr Name
e1 Expr Name
e2 Expr Name
e3 ->
      do Expr
e1'      <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e1 (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tBit TypeSource
TypeOfIfCondExpr (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e1))
         Expr
e2'      <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e2 TypeWithSource
tGoal
         Expr
e3'      <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e3 TypeWithSource
tGoal
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIf Expr
e1' Expr
e2' Expr
e3')

    P.EWhere Expr Name
e [Decl Name]
ds ->
      do (Expr
e1,[DeclGroup]
ds1) <- [Decl Name] -> InferM Expr -> InferM (Expr, [DeclGroup])
forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
         Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> [DeclGroup] -> Expr
EWhere Expr
e1 [DeclGroup]
ds1)

    P.ETyped Expr Name
e Type Name
t ->
      do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
         Expr
e' <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tSig TypeSource
TypeFromUserAnnotation (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
expr))
         Prop -> TypeWithSource -> InferM ()
checkHasType Prop
tSig TypeWithSource
tGoal
         Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'

    P.ETypeVal Type Name
t ->
      do Range
l <- InferM Range
curRange
         Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"number"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> [TypeInst Name] -> Expr Name
forall n. Expr n -> [TypeInst n] -> Expr n
P.EAppT Expr Name
prim
                  [Named (Type Name) -> TypeInst Name
forall name. Named (Type name) -> TypeInst name
P.NamedInst
                   P.Named { name :: Located Ident
name = Range -> Ident -> Located Ident
forall a. Range -> a -> Located a
Located Range
l (String -> Ident
packIdent String
"val")
                           , value :: Type Name
value = Type Name
t }]) TypeWithSource
tGoal

    P.EFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e -> FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
desc [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal

    P.ELocated Expr Name
e Range
r  ->
      do Expr
e' <- Range -> InferM Expr -> InferM Expr
forall a. Range -> InferM a -> InferM a
inRange Range
r (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal)
         Bool
cs <- InferM Bool
getCallStacks
         if Bool
cs then Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range -> Expr -> Expr
ELocated Range
r Expr
e') else Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e'

    P.ESplit Expr Name
e ->
      do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim String
"splitAt"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal

    P.EInfix Expr Name
a Located Name
op Fixity
_ Expr Name
b -> Expr Name -> TypeWithSource -> InferM Expr
checkE (Name -> Expr Name
forall n. n -> Expr n
P.EVar (Located Name -> Name
forall a. Located a -> a
thing Located Name
op) Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
a Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
`P.EApp` Expr Name
b) TypeWithSource
tGoal

    P.EPrefix PrefixOp
op Expr Name
e ->
      do Expr Name
prim <- String -> InferM (Expr Name)
mkPrim case PrefixOp
op of
           PrefixOp
P.PrefixNeg        -> String
"negate"
           PrefixOp
P.PrefixComplement -> String
"complement"
         Expr Name -> TypeWithSource -> InferM Expr
checkE (Expr Name -> Expr Name -> Expr Name
forall n. Expr n -> Expr n -> Expr n
P.EApp Expr Name
prim Expr Name
e) TypeWithSource
tGoal

    P.ECase Expr Name
e [CaseAlt Name]
as ->
     do Prop
et   <- TypeSource -> Kind -> InferM Prop
newType TypeSource
CasedExpression Kind
KType
        [(Range, Maybe Ident, CaseAlt)]
alts <- [CaseAlt Name]
-> (CaseAlt Name -> InferM (Range, Maybe Ident, CaseAlt))
-> InferM [(Range, Maybe Ident, CaseAlt)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CaseAlt Name]
as \CaseAlt Name
a -> CaseAlt Name
-> Prop -> TypeWithSource -> InferM (Range, Maybe Ident, CaseAlt)
checkCaseAlt CaseAlt Name
a Prop
et TypeWithSource
tGoal
        Range
rng  <- InferM Range
curRange
        Expr
e1   <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
et TypeSource
CasedExpression (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
rng))

        -- Check for overlapping cases that follow default patterns, e.g.,
        --
        --   enum Foo = A | B
        --   f : Foo -> Bit
        --   f l =
        --     case l of
        --       _ -> True
        --       B -> False
        --
        -- In this example, the `B` case overlaps the catch-all `_` case.
        let defltAltAndOthers :: [(Range, Maybe Ident, CaseAlt)]
defltAltAndOthers = ((Range, Maybe Ident, CaseAlt) -> Bool)
-> [(Range, Maybe Ident, CaseAlt)]
-> [(Range, Maybe Ident, CaseAlt)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\(Range
_,Maybe Ident
x,CaseAlt
_) -> Maybe Ident -> Bool
forall a. Maybe a -> Bool
isJust Maybe Ident
x) [(Range, Maybe Ident, CaseAlt)]
alts
        Maybe (Range, Maybe Ident, CaseAlt)
defltAlt <-
          case [(Range, Maybe Ident, CaseAlt)]
defltAltAndOthers of
            [] ->
              Maybe (Range, Maybe Ident, CaseAlt)
-> InferM (Maybe (Range, Maybe Ident, CaseAlt))
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Range, Maybe Ident, CaseAlt)
forall a. Maybe a
Nothing
            defltAlt :: (Range, Maybe Ident, CaseAlt)
defltAlt@(Range
_,Maybe Ident
defltPat,CaseAlt
_):[(Range, Maybe Ident, CaseAlt)]
otherAlts -> do
              Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Range, Maybe Ident, CaseAlt)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Range, Maybe Ident, CaseAlt)]
otherAlts) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
                Error -> InferM ()
recordError (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$
                Maybe Ident -> [Range] -> Error
OverlappingPat Maybe Ident
defltPat [ Range
r | (Range
r,Maybe Ident
_,CaseAlt
_) <- [(Range, Maybe Ident, CaseAlt)]
defltAltAndOthers ]
              Maybe (Range, Maybe Ident, CaseAlt)
-> InferM (Maybe (Range, Maybe Ident, CaseAlt))
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Range, Maybe Ident, CaseAlt)
-> Maybe (Range, Maybe Ident, CaseAlt)
forall a. a -> Maybe a
Just (Range, Maybe Ident, CaseAlt)
defltAlt)

        -- Check that there are no overlapping patterns among the case
        -- alternatives, e.g.,
        --
        --   enum Foo = A | B
        --   g : Foo -> Bit
        --   g l =
        --     case l of
        --       A -> True
        --       B -> True
        --       B -> False
        --
        -- In this example, the two `B` cases overlap.
        let mp1 :: Map (Maybe Ident) [(Range, CaseAlt)]
mp1 = ([(Range, CaseAlt)] -> [(Range, CaseAlt)] -> [(Range, CaseAlt)])
-> [(Maybe Ident, [(Range, CaseAlt)])]
-> Map (Maybe Ident) [(Range, CaseAlt)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [(Range, CaseAlt)] -> [(Range, CaseAlt)] -> [(Range, CaseAlt)]
forall a. [a] -> [a] -> [a]
(++) [ (Maybe Ident
x,[(Range
r,CaseAlt
y)]) | (Range
r,Maybe Ident
x,CaseAlt
y) <- [(Range, Maybe Ident, CaseAlt)]
alts ]
        [(Maybe Ident, [(Range, CaseAlt)])]
-> ((Maybe Ident, [(Range, CaseAlt)]) -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map (Maybe Ident) [(Range, CaseAlt)]
-> [(Maybe Ident, [(Range, CaseAlt)])]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Maybe Ident) [(Range, CaseAlt)]
mp1) \(Maybe Ident
mb,[(Range, CaseAlt)]
cs) ->
          case [(Range, CaseAlt)]
cs of
            [(Range, CaseAlt)
_] -> () -> InferM ()
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            [(Range, CaseAlt)]
_   -> Error -> InferM ()
recordError (Maybe Ident -> [Range] -> Error
OverlappingPat Maybe Ident
mb [ Range
r | (Range
r,CaseAlt
_) <- [(Range, CaseAlt)]
cs ])

        -- Check that the type of the scrutinee is unambiguously an enum.
        Prop
et' <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
et
        [EnumCon]
cons <- case Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e of
                 Just Range
r -> Range -> InferM [EnumCon] -> InferM [EnumCon]
forall a. Range -> InferM a -> InferM a
inRange Range
r (Prop -> InferM [EnumCon]
expectEnum Prop
et')
                 Maybe Range
Nothing -> Prop -> InferM [EnumCon]
expectEnum Prop
et'

        -- Check that the case expression covers all possible constructors.
        -- If there is a default case, there is no need to check anything,
        -- since the default case will catch any constructors that weren't
        -- explicitly matched on.
        case Maybe (Range, Maybe Ident, CaseAlt)
defltAlt of
          Just (Range, Maybe Ident, CaseAlt)
_ -> () -> InferM ()
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Maybe (Range, Maybe Ident, CaseAlt)
Nothing ->
            let uncoveredCons :: [EnumCon]
uncoveredCons =
                  (EnumCon -> Bool) -> [EnumCon] -> [EnumCon]
forall a. (a -> Bool) -> [a] -> [a]
filter
                    (\EnumCon
con -> Maybe Ident -> Map (Maybe Ident) [(Range, CaseAlt)] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember (Ident -> Maybe Ident
forall a. a -> Maybe a
Just (Name -> Ident
nameIdent (EnumCon -> Name
ecName EnumCon
con))) Map (Maybe Ident) [(Range, CaseAlt)]
mp1)
                    [EnumCon]
cons in
            Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([EnumCon] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EnumCon]
uncoveredCons) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
              Error -> InferM ()
recordError (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ [Name] -> Error
UncoveredConPat ([Name] -> Error) -> [Name] -> Error
forall a b. (a -> b) -> a -> b
$ (EnumCon -> Name) -> [EnumCon] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map EnumCon -> Name
ecName [EnumCon]
uncoveredCons

        let dflt :: Maybe CaseAlt
dflt = ((Range, Maybe Ident, CaseAlt) -> CaseAlt)
-> Maybe (Range, Maybe Ident, CaseAlt) -> Maybe CaseAlt
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Range
_,Maybe Ident
_,CaseAlt
y) -> CaseAlt
y) Maybe (Range, Maybe Ident, CaseAlt)
defltAlt
        let arms :: Map Ident CaseAlt
arms = [(Ident, CaseAlt)] -> Map Ident CaseAlt
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Ident
i,CaseAlt
a) | (Range
_,Just Ident
i, CaseAlt
a) <- [(Range, Maybe Ident, CaseAlt)]
alts ]
        Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> Map Ident CaseAlt -> Maybe CaseAlt -> Expr
ECase Expr
e1 Map Ident CaseAlt
arms Maybe CaseAlt
dflt)

    P.EParens Expr Name
e -> Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal


checkCaseAlt ::
  P.CaseAlt Name -> Type -> TypeWithSource ->
  InferM (Range, Maybe Ident, CaseAlt)
checkCaseAlt :: CaseAlt Name
-> Prop -> TypeWithSource -> InferM (Range, Maybe Ident, CaseAlt)
checkCaseAlt (P.CaseAlt Pattern Name
pat Expr Name
e) Prop
srcT TypeWithSource
resT =
  case Pattern Name
pat of
    P.PCon Located Name
c [Pattern Name]
ps ->
      Range
-> InferM (Range, Maybe Ident, CaseAlt)
-> InferM (Range, Maybe Ident, CaseAlt)
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
c) (InferM (Range, Maybe Ident, CaseAlt)
 -> InferM (Range, Maybe Ident, CaseAlt))
-> InferM (Range, Maybe Ident, CaseAlt)
-> InferM (Range, Maybe Ident, CaseAlt)
forall a b. (a -> b) -> a -> b
$
      do ([Prop]
_tArgs,Int
_pArgs,[Prop]
fTs,Prop
cresT) <- Name -> InferM ([Prop], Int, [Prop], Prop)
instantiatePCon (Located Name -> Name
forall a. Located a -> a
thing Located Name
c)
         -- XXX: should we store these somewhere?

         let have :: Int
have = [Pattern Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern Name]
ps
             need :: Int
need = [Prop] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
fTs
         Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
have Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
need) (Error -> InferM ()
recordError (Int -> Int -> Error
InvalidConPat Int
have Int
need))
         let expect :: TypeWithSource
expect = WithSource
                        { twsType :: Prop
twsType = Prop
srcT
                        , twsRange :: Maybe Range
twsRange = Range -> Maybe Range
forall a. a -> Maybe a
Just (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
c)
                        , twsSource :: TypeSource
twsSource = TypeSource
ConPat
                        }
         ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
expect Prop
cresT
         [(Name, Located Prop)]
xs <- (Pattern Name -> Prop -> InferM (Name, Located Prop))
-> [Pattern Name] -> [Prop] -> InferM [(Name, Located Prop)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Pattern Name -> Prop -> InferM (Name, Located Prop)
checkNested [Pattern Name]
ps [Prop]
fTs
         Expr
e1 <- Map Name (Located Prop) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes ([(Name, Located Prop)] -> Map Name (Located Prop)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name, Located Prop)]
xs) (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
resT)
         (Range, Maybe Ident, CaseAlt)
-> InferM (Range, Maybe Ident, CaseAlt)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
c, Ident -> Maybe Ident
forall a. a -> Maybe a
Just (Name -> Ident
nameIdent (Located Name -> Name
forall a. Located a -> a
thing Located Name
c)), [(Name, Located Prop)] -> Expr -> CaseAlt
mkAlt [(Name, Located Prop)]
xs Expr
e1)

    P.PVar Located Name
x ->
      do let xty :: (Name, Located Prop)
xty = (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Range -> Prop -> Located Prop
forall a. Range -> a -> Located a
Located (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x) Prop
srcT)
         Expr
e1 <- (Name, Located Prop) -> InferM Expr -> InferM Expr
forall a. (Name, Located Prop) -> InferM a -> InferM a
withMonoType (Name, Located Prop)
xty (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
resT)
         (Range, Maybe Ident, CaseAlt)
-> InferM (Range, Maybe Ident, CaseAlt)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x, Maybe Ident
forall a. Maybe a
Nothing, [(Name, Located Prop)] -> Expr -> CaseAlt
mkAlt [(Name, Located Prop)
xty] Expr
e1)

    P.PLocated Pattern Name
p Range
r -> Range
-> InferM (Range, Maybe Ident, CaseAlt)
-> InferM (Range, Maybe Ident, CaseAlt)
forall a. Range -> InferM a -> InferM a
inRange Range
r (CaseAlt Name
-> Prop -> TypeWithSource -> InferM (Range, Maybe Ident, CaseAlt)
checkCaseAlt (Pattern Name -> Expr Name -> CaseAlt Name
forall n. Pattern n -> Expr n -> CaseAlt n
P.CaseAlt Pattern Name
p Expr Name
e) Prop
srcT TypeWithSource
resT)

    P.PTyped Pattern Name
p Type Name
t ->
      do Prop
t1 <- Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KType)
         Range
rng <- InferM Range
curRange
         ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
           TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t1 TypeSource
TypeFromUserAnnotation (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
rng)) Prop
srcT
         CaseAlt Name
-> Prop -> TypeWithSource -> InferM (Range, Maybe Ident, CaseAlt)
checkCaseAlt (Pattern Name -> Expr Name -> CaseAlt Name
forall n. Pattern n -> Expr n -> CaseAlt n
P.CaseAlt Pattern Name
p Expr Name
e) Prop
t1 TypeWithSource
resT

    Pattern Name
_ -> String -> [String] -> InferM (Range, Maybe Ident, CaseAlt)
forall a. HasCallStack => String -> [String] -> a
panic String
"checkCaseAlt" [String
"Unexpected pattern"]
  where
  checkNested :: Pattern Name -> Prop -> InferM (Name, Located Prop)
checkNested Pattern Name
p Prop
ty =
    case Pattern Name
p of
      P.PVar Located Name
x -> (Name, Located Prop) -> InferM (Name, Located Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Range -> Prop -> Located Prop
forall a. Range -> a -> Located a
Located (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x) Prop
ty)
      P.PLocated Pattern Name
p1 Range
r -> Range -> InferM (Name, Located Prop) -> InferM (Name, Located Prop)
forall a. Range -> InferM a -> InferM a
inRange Range
r (Pattern Name -> Prop -> InferM (Name, Located Prop)
checkNested Pattern Name
p1 Prop
ty)
      P.PTyped Pattern Name
p1 Type Name
t ->
        do Prop
t1 <- Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
t (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KType)
           Range
rng <- InferM Range
curRange
           ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
             TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t1 TypeSource
TypeFromUserAnnotation (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
rng)) Prop
ty
           Pattern Name -> Prop -> InferM (Name, Located Prop)
checkNested Pattern Name
p1 Prop
t1
      Pattern Name
_ -> String -> [String] -> InferM (Name, Located Prop)
forall a. HasCallStack => String -> [String] -> a
panic String
"checkNested" [String
"Unexpected pattern"]



  mkAlt :: [(Name, Located Prop)] -> Expr -> CaseAlt
mkAlt [(Name, Located Prop)]
xs = [(Name, Prop)] -> Expr -> CaseAlt
CaseAlt [ (Name
x, Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t) | (Name
x,Located Prop
t) <- [(Name, Located Prop)]
xs ]


checkRecUpd ::
  Maybe (P.Expr Name) -> [ P.UpdField Name ] -> TypeWithSource -> InferM Expr
checkRecUpd :: Maybe (Expr Name)
-> [UpdField Name] -> TypeWithSource -> InferM Expr
checkRecUpd Maybe (Expr Name)
mb [UpdField Name]
fs TypeWithSource
tGoal =
  case Maybe (Expr Name)
mb of

    -- { _ | fs } ~~>  \r -> { r | fs }
    Maybe (Expr Name)
Nothing ->
      do Name
r <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"r")
         let p :: Pattern Name
p  = Located Name -> Pattern Name
forall n. Located n -> Pattern n
P.PVar Located { srcRange :: Range
srcRange = Name -> Range
nameLoc Name
r, thing :: Name
thing = Name
r }
             fe :: Expr Name
fe = FunDesc Name -> [Pattern Name] -> Expr Name -> Expr Name
forall n. FunDesc n -> [Pattern n] -> Expr n -> Expr n
P.EFun FunDesc Name
forall n. FunDesc n
P.emptyFunDesc [Pattern Name
p] (Maybe (Expr Name) -> [UpdField Name] -> Expr Name
forall n. Maybe (Expr n) -> [UpdField n] -> Expr n
P.EUpd (Expr Name -> Maybe (Expr Name)
forall a. a -> Maybe a
Just (Name -> Expr Name
forall n. n -> Expr n
P.EVar Name
r)) [UpdField Name]
fs)
         Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
fe TypeWithSource
tGoal

    Just Expr Name
e ->
      do Expr
e1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
         (Expr, Maybe Range) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Maybe Range) -> Expr)
-> InferM (Expr, Maybe Range) -> InferM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Expr, Maybe Range)
 -> UpdField Name -> InferM (Expr, Maybe Range))
-> (Expr, Maybe Range)
-> [UpdField Name]
-> InferM (Expr, Maybe Range)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Expr, Maybe Range) -> UpdField Name -> InferM (Expr, Maybe Range)
doUpd (Expr
e1, Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e) [UpdField Name]
fs

  where
  doUpd :: (Expr, Maybe Range) -> UpdField Name -> InferM (Expr, Maybe Range)
doUpd (Expr
e,Maybe Range
eloc) (P.UpdField UpdHow
how [Located Selector]
sels Expr Name
v) =
    case [Located Selector]
sels of
      [Located Selector
l] ->
        case UpdHow
how of
          UpdHow
P.UpdSet ->
            do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
               Prop
ft <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
               Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ft TypeSource
src Maybe Range
eloc)
               HasGoalSln
d  <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Prop
twsType TypeWithSource
tGoal) Prop
ft
               (Expr, Maybe Range) -> InferM (Expr, Maybe Range)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e Expr
v1, Maybe Range
eloc Maybe Range -> Maybe Range -> Maybe Range
`rCombMaybe` Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
v)
          UpdHow
P.UpdFun ->
             do let src :: TypeSource
src = Selector -> TypeSource
selSrc Selector
s
                Prop
ft <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
KType
                Expr
v1 <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
v (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tFun Prop
ft Prop
ft) TypeSource
src Maybe Range
eloc)
                -- XXX: ^ may be used a different src?
                HasGoalSln
d  <- Selector -> Prop -> Prop -> InferM HasGoalSln
newHasGoal Selector
s (TypeWithSource -> Prop
twsType TypeWithSource
tGoal) Prop
ft
                Name
tmp <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"rf")
                let e' :: Expr
e' = Name -> Expr
EVar Name
tmp
                (Expr, Maybe Range) -> InferM (Expr, Maybe Range)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d Expr
e' (Expr -> Expr -> Expr
EApp Expr
v1 (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d Expr
e'))
                       Expr -> [DeclGroup] -> Expr
`EWhere`
                       [  Decl -> DeclGroup
NonRecursive
                          Decl { dName :: Name
dName        = Name
tmp
                               , dSignature :: Schema
dSignature   = Prop -> Schema
tMono (TypeWithSource -> Prop
twsType TypeWithSource
tGoal)
                               , dDefinition :: DeclDef
dDefinition  = Expr -> DeclDef
DExpr Expr
e
                               , dPragmas :: [Pragma]
dPragmas     = []
                               , dInfix :: Bool
dInfix       = Bool
False
                               , dFixity :: Maybe Fixity
dFixity      = Maybe Fixity
forall a. Maybe a
Nothing
                               , dDoc :: Maybe Text
dDoc         = Maybe Text
forall a. Maybe a
Nothing
                               } ]
                      , Maybe Range
eloc Maybe Range -> Maybe Range -> Maybe Range
`rCombMaybe` Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
v )

        where s :: Selector
s = Located Selector -> Selector
forall a. Located a -> a
thing Located Selector
l
      [Located Selector]
_ -> String -> [String] -> InferM (Expr, Maybe Range)
forall a. HasCallStack => String -> [String] -> a
panic String
"checkRecUpd/doUpd" [ String
"Expected exactly 1 field label"
                                     , String
"Got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Located Selector] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Located Selector]
sels)
                                     ]


expectSeq :: TypeWithSource -> InferM (Type,Type)
expectSeq :: TypeWithSource -> InferM (Prop, Prop)
expectSeq tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
  case Prop
ty of

    TUser Name
_ [Prop]
_ Prop
ty' ->
         TypeWithSource -> InferM (Prop, Prop)
expectSeq (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)

    TCon (TC TC
TCSeq) [Prop
a,Prop
b] ->
         (Prop, Prop) -> InferM (Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)

    TVar TVar
_ ->
      do tys :: (Prop, Prop)
tys@(Prop
a,Prop
b) <- InferM (Prop, Prop)
genTys
         ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (Prop -> Prop -> Prop
tSeq Prop
a Prop
b)
         (Prop, Prop) -> InferM (Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys

    Prop
_ ->
      do tys :: (Prop, Prop)
tys@(Prop
a,Prop
b) <- InferM (Prop, Prop)
genTys
         Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty (Prop -> Prop -> Prop
tSeq Prop
a Prop
b))
         (Prop, Prop) -> InferM (Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop, Prop)
tys
  where
  genTys :: InferM (Prop, Prop)
genTys =
    do Prop
a <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
       Prop
b <- TypeSource -> Kind -> InferM Prop
newType TypeSource
TypeOfSeqElement Kind
KType
       (Prop, Prop) -> InferM (Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
a,Prop
b)


expectTuple :: Int -> TypeWithSource -> InferM [Type]
expectTuple :: Int -> TypeWithSource -> InferM [Prop]
expectTuple Int
n tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
  case Prop
ty of

    TUser Name
_ [Prop]
_ Prop
ty' ->
         Int -> TypeWithSource -> InferM [Prop]
expectTuple Int
n (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)

    TCon (TC (TCTuple Int
n')) [Prop]
tys | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n' ->
         [Prop] -> InferM [Prop]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys

    TVar TVar
_ ->
      do [Prop]
tys <- InferM [Prop]
genTys
         ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal ([Prop] -> Prop
tTuple [Prop]
tys)
         [Prop] -> InferM [Prop]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys

    Prop
_ ->
      do [Prop]
tys <- InferM [Prop]
genTys
         Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty ([Prop] -> Prop
tTuple [Prop]
tys))
         [Prop] -> InferM [Prop]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return [Prop]
tys

  where
  genTys :: InferM [Prop]
genTys =[Int] -> (Int -> InferM Prop) -> InferM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 ] ((Int -> InferM Prop) -> InferM [Prop])
-> (Int -> InferM Prop) -> InferM [Prop]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> TypeSource -> Kind -> InferM Prop
newType (Int -> TypeSource
TypeOfTupleField Int
i) Kind
KType


expectRec ::
  RecordMap Ident (Range, a) ->
  TypeWithSource ->
  InferM (RecordMap Ident (a, Type))
expectRec :: forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec RecordMap Ident (Range, a)
fs tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
  case Prop
ty of

    TUser Name
_ [Prop]
_ Prop
ty' ->
         RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
forall a.
RecordMap Ident (Range, a)
-> TypeWithSource -> InferM (RecordMap Ident (a, Prop))
expectRec RecordMap Ident (Range, a)
fs (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)

    TRec RecordMap Ident Prop
ls
      | Right RecordMap Ident (a, Prop)
r <- (Ident -> (Range, a) -> Prop -> (a, Prop))
-> RecordMap Ident (Range, a)
-> RecordMap Ident Prop
-> Either (Either Ident Ident) (RecordMap Ident (a, Prop))
forall a b c d.
Ord a =>
(a -> b -> c -> d)
-> RecordMap a b
-> RecordMap a c
-> Either (Either a a) (RecordMap a d)
zipRecords (\Ident
_ (Range
_rng,a
v) Prop
t -> (a
v,Prop
t)) RecordMap Ident (Range, a)
fs RecordMap Ident Prop
ls -> RecordMap Ident (a, Prop) -> InferM (RecordMap Ident (a, Prop))
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RecordMap Ident (a, Prop)
r

    Prop
_ ->
      do RecordMap Ident (a, Prop)
res <- (Ident -> (Range, a) -> InferM (a, Prop))
-> RecordMap Ident (Range, a) -> InferM (RecordMap Ident (a, Prop))
forall (t :: * -> *) a b c.
Applicative t =>
(a -> b -> t c) -> RecordMap a b -> t (RecordMap a c)
traverseRecordMap
                  (\Ident
nm (Range
_rng,a
v) ->
                       do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Ident -> TypeSource
TypeOfRecordField Ident
nm) Kind
KType
                          (a, Prop) -> InferM (a, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
v, Prop
t))
                  RecordMap Ident (Range, a)
fs
         let tys :: RecordMap Ident Prop
tys = ((a, Prop) -> Prop)
-> RecordMap Ident (a, Prop) -> RecordMap Ident Prop
forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Prop) -> Prop
forall a b. (a, b) -> b
snd RecordMap Ident (a, Prop)
res
         case Prop
ty of
           TVar TVFree{} -> do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
tys)
                               ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
           Prop
_ -> Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
tys))
         RecordMap Ident (a, Prop) -> InferM (RecordMap Ident (a, Prop))
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return RecordMap Ident (a, Prop)
res


-- | Retrieve the constructors from a type that is expected to be unambiguously
-- an enum, throwing an error if this is not the case.
expectEnum :: Type -> InferM [EnumCon]
expectEnum :: Prop -> InferM [EnumCon]
expectEnum Prop
ty =
  case Prop
ty of
    TUser Name
_ [Prop]
_ Prop
ty' ->
      Prop -> InferM [EnumCon]
expectEnum Prop
ty'

    TNominal NominalType
nt [Prop]
_
      |  Enum [EnumCon]
ecs <- NominalType -> NominalTypeDef
ntDef NominalType
nt
      -> [EnumCon] -> InferM [EnumCon]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [EnumCon]
ecs

    Prop
_ -> do
      Error -> InferM ()
recordError (Prop -> Error
EnumTypeMismatch Prop
ty)
      [EnumCon] -> InferM [EnumCon]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

expectFin :: Int -> TypeWithSource -> InferM ()
expectFin :: Int -> TypeWithSource -> InferM ()
expectFin Int
n tGoal :: TypeWithSource
tGoal@(WithSource Prop
ty TypeSource
src Maybe Range
rng) =
  case Prop
ty of

    TUser Name
_ [Prop]
_ Prop
ty' ->
         Int -> TypeWithSource -> InferM ()
expectFin Int
n (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty' TypeSource
src Maybe Range
rng)

    TCon (TC (TCNum Integer
n')) [] | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' ->
         () -> InferM ()
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    Prop
_ -> ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
n)

expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)
expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Prop], Prop)
expectFun Maybe Name
mbN Int
n (WithSource Prop
ty0 TypeSource
src Maybe Range
rng)  = [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [] Int
n Prop
ty0
  where

  go :: [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [Prop]
tys Int
arity Prop
ty
    | Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
      case Prop
ty of

        TUser Name
_ [Prop]
_ Prop
ty' ->
             [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go [Prop]
tys Int
arity Prop
ty'

        TCon (TC TC
TCFun) [Prop
a,Prop
b] ->
             [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
go (Prop
aProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop]
tys) (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Prop
b

        Prop
_ ->
          do [Prop]
args <- Int -> InferM [Prop]
genArgs Int
arity
             Prop
res  <- TypeSource -> Kind -> InferM Prop
newType TypeSource
TypeOfRes Kind
KType
             case Prop
ty of
               TVar TVFree{} ->
                  do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
ty TypeSource
src Maybe Range
rng) ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
res [Prop]
args)
                     ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType  [Prop]
ps
               Prop
_ -> Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rng
                        (TypeSource -> Path -> Prop -> Prop -> Error
TypeMismatch TypeSource
src Path
rootPath Prop
ty ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
res [Prop]
args))
             ([Prop], Prop) -> InferM ([Prop], Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
tys [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
args, Prop
res)

    | Bool
otherwise =
      ([Prop], Prop) -> InferM ([Prop], Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
tys, Prop
ty)

  genArgs :: Int -> InferM [Prop]
genArgs Int
arity = [Int] -> (Int -> InferM Prop) -> InferM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
1 .. Int
arity ] ((Int -> InferM Prop) -> InferM [Prop])
-> (Int -> InferM Prop) -> InferM [Prop]
forall a b. (a -> b) -> a -> b
$
                    \ Int
ix -> TypeSource -> Kind -> InferM Prop
newType (ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
mbN (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
ix))) Kind
KType


checkHasType :: Type -> TypeWithSource -> InferM ()
checkHasType :: Prop -> TypeWithSource -> InferM ()
checkHasType Prop
inferredType TypeWithSource
tGoal =
  do [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal Prop
inferredType
     case [Prop]
ps of
       [] -> () -> InferM ()
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [Prop]
_  -> ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps


checkFun ::
  P.FunDesc Name -> [P.Pattern Name] ->
  P.Expr Name -> TypeWithSource -> InferM Expr
checkFun :: FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun FunDesc Name
_    [] Expr Name
e TypeWithSource
tGoal = Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e TypeWithSource
tGoal
checkFun (P.FunDesc Maybe Name
fun Int
offset) [Pattern Name]
ps Expr Name
e TypeWithSource
tGoal =
  InferM Expr -> InferM Expr
forall a. InferM a -> InferM a
inNewScope
  do let descs :: [TypeSource]
descs = [ ArgDescr -> TypeSource
TypeOfArg (Maybe Name -> Maybe Int -> ArgDescr
ArgDescr Maybe Name
fun (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)) | Int
n <- [ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset .. ] ]

     ([Prop]
tys,Prop
tRes) <- Maybe Name -> Int -> TypeWithSource -> InferM ([Prop], Prop)
expectFun Maybe Name
fun ([Pattern Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern Name]
ps) TypeWithSource
tGoal
     let srcs :: [TypeWithSource]
srcs = (Prop -> TypeSource -> Maybe Range -> TypeWithSource)
-> [Prop] -> [TypeSource] -> [Maybe Range] -> [TypeWithSource]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource [Prop]
tys [TypeSource]
descs ((Pattern Name -> Maybe Range) -> [Pattern Name] -> [Maybe Range]
forall a b. (a -> b) -> [a] -> [b]
map Pattern Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc [Pattern Name]
ps)
     [Located Name]
largs      <- [InferM (Located Name)] -> InferM [Located Name]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ((Pattern Name -> TypeWithSource -> InferM (Located Name))
-> [Pattern Name] -> [TypeWithSource] -> [InferM (Located Name)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP [Pattern Name]
ps [TypeWithSource]
srcs)
     let ds :: Map Name (Located Prop)
ds = [(Name, Located Prop)] -> Map Name (Located Prop)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Located Name
x { thing = t }) | (Located Name
x,Prop
t) <- [Located Name] -> [Prop] -> [(Located Name, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
     Expr
e1 <- Map Name (Located Prop) -> InferM Expr -> InferM Expr
forall a. Map Name (Located Prop) -> InferM a -> InferM a
withMonoTypes Map Name (Located Prop)
ds
              (Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tRes TypeSource
TypeOfRes (TypeWithSource -> Maybe Range
twsRange TypeWithSource
tGoal)))

     let args :: [(Name, Prop)]
args = [ (Located Name -> Name
forall a. Located a -> a
thing Located Name
x, Prop
t) | (Located Name
x,Prop
t) <- [Located Name] -> [Prop] -> [(Located Name, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Located Name]
largs [Prop]
tys ]
     Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, Prop) -> Expr -> Expr) -> Expr -> [(Name, Prop)] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
x,Prop
t) Expr
b -> Name -> Prop -> Expr -> Expr
EAbs Name
x Prop
t Expr
b) Expr
e1 [(Name, Prop)]
args)


{-| The type the is the smallest of all -}
smallest :: [Type] -> InferM Type
smallest :: [Prop] -> InferM Prop
smallest []   = TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
smallest [Prop
t]  = Prop -> InferM Prop
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
t
smallest [Prop]
ts   = do Prop
a <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfSeq Kind
KNum
                   ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Prop
a Prop -> Prop -> Prop
=#= (Prop -> Prop -> Prop) -> [Prop] -> Prop
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Prop -> Prop -> Prop
tMin [Prop]
ts ]
                   Prop -> InferM Prop
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
a

checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP :: Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p tGoal :: TypeWithSource
tGoal@(WithSource Prop
_ TypeSource
src Maybe Range
rng0) =
  do (Name
x, Located Prop
t) <- Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
p
     [Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify TypeWithSource
tGoal (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t)
     let rngMb :: Maybe Range
rngMb = Pattern Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Pattern Name
p Maybe Range -> Maybe Range -> Maybe Range
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe Range
rng0
         rng :: Range
rng   = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange Maybe Range
rngMb
     let mkErr :: Prop -> InferM ()
mkErr = Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
rngMb (Error -> InferM ()) -> (Prop -> Error) -> Prop -> InferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Goal] -> Error
UnsolvedGoals ([Goal] -> Error) -> (Prop -> [Goal]) -> Prop -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Goal -> [Goal] -> [Goal]
forall a. a -> [a] -> [a]
:[])
                                                   (Goal -> [Goal]) -> (Prop -> Goal) -> Prop -> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintSource -> Range -> Prop -> Goal
Goal (TypeSource -> ConstraintSource
CtPattern TypeSource
src) Range
rng
     (Prop -> InferM ()) -> [Prop] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> InferM ()
mkErr [Prop]
ps
     Located Name -> InferM (Located Name)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> Name -> Located Name
forall a. Range -> a -> Located a
Located (Located Prop -> Range
forall a. Located a -> Range
srcRange Located Prop
t) Name
x)

{-| Infer the type of a pattern.  Assumes that the pattern will be just
a variable. -}
inferP :: P.Pattern Name -> InferM (Name, Located Type)
inferP :: Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
pat =
  case Pattern Name
pat of

    P.PVar Located Name
x0 ->
      do Prop
a   <- Range -> InferM Prop -> InferM Prop
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
x0) (TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0)) Kind
KType)
         (Name, Located Prop) -> InferM (Name, Located Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
x0, Located Name
x0 { thing = a })

    P.PTyped Pattern Name
p Type Name
t ->
      do Prop
tSig <- Type Name -> Kind -> InferM Prop
checkTypeOfKind Type Name
t Kind
KType
         Located Name
ln   <- Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP Pattern Name
p (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
tSig TypeSource
TypeFromUserAnnotation (Type Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Type Name
t))
         (Name, Located Prop) -> InferM (Name, Located Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Located Name -> Name
forall a. Located a -> a
thing Located Name
ln, Located Name
ln { thing = tSig })

    Pattern Name
_ -> String -> [String] -> InferM (Name, Located Prop)
forall a. String -> [String] -> a
tcPanic String
"inferP" [ String
"Unexpected pattern:", Pattern Name -> String
forall a. Show a => a -> String
show Pattern Name
pat ]



-- | Infer the type of one match in a list comprehension.
inferMatch :: P.Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch :: Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch (P.Match Pattern Name
p Expr Name
e) =
  do (Name
x,Located Prop
t) <- Pattern Name -> InferM (Name, Located Prop)
inferP Pattern Name
p
     Prop
n     <- TypeSource -> Kind -> InferM Prop
newType TypeSource
LenOfCompGen Kind
KNum
     Expr
e'    <- Expr Name -> TypeWithSource -> InferM Expr
checkE Expr Name
e (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (Prop -> Prop -> Prop
tSeq Prop
n (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t)) TypeSource
GeneratorOfListComp
                                   (Expr Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr Name
e))
     (Match, Name, Located Prop, Prop)
-> InferM (Match, Name, Located Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Prop -> Prop -> Expr -> Match
From Name
x Prop
n (Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
t) Expr
e', Name
x, Located Prop
t, Prop
n)

inferMatch (P.MatchLet Bind Name
b)
  | Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono Bind Name
b =
  do let rng :: Range
rng = Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
     Prop
a <- Range -> InferM Prop -> InferM Prop
forall a. Range -> InferM a -> InferM a
inRange Range
rng (TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) Kind
KType)
     Decl
b1 <- Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
a
     (Match, Name, Located Prop, Prop)
-> InferM (Match, Name, Located Prop, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Match
Let Decl
b1, Decl -> Name
dName Decl
b1, Range -> Prop -> Located Prop
forall a. Range -> a -> Located a
Located (Located Name -> Range
forall a. Located a -> Range
srcRange (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)) Prop
a, Int -> Prop
forall a. Integral a => a -> Prop
tNum (Int
1::Int))

  | Bool
otherwise = String -> [String] -> InferM (Match, Name, Located Prop, Prop)
forall a. String -> [String] -> a
tcPanic String
"inferMatch"
                      [ String
"Unexpected polymorphic match let:", Bind Name -> String
forall a. Show a => a -> String
show Bind Name
b ]

-- | Infer the type of one arm of a list comprehension.
inferCArm :: Int -> [P.Match Name] -> InferM
              ( [Match]
              , Map Name (Located Type)-- defined vars
              , Type                   -- length of sequence
              )

inferCArm :: Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm Int
_ [] = String
-> [String] -> InferM ([Match], Map Name (Located Prop), Prop)
forall a. HasCallStack => String -> [String] -> a
panic String
"inferCArm" [ String
"Empty comprehension arm" ]
inferCArm Int
_ [Match Name
m] =
  do (Match
m1, Name
x, Located Prop
t, Prop
n) <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
     ([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Match
m1], Name -> Located Prop -> Map Name (Located Prop)
forall k a. k -> a -> Map k a
Map.singleton Name
x Located Prop
t, Prop
n)

inferCArm Int
armNum (Match Name
m : [Match Name]
ms) =
  do (Match
m1, Name
x, Located Prop
t, Prop
n)  <- Match Name -> InferM (Match, Name, Located Prop, Prop)
inferMatch Match Name
m
     ([Match]
ms', Map Name (Located Prop)
ds, Prop
n')  <- (Name, Located Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall a. (Name, Located Prop) -> InferM a -> InferM a
withMonoType (Name
x,Located Prop
t) (Int
-> [Match Name] -> InferM ([Match], Map Name (Located Prop), Prop)
inferCArm Int
armNum [Match Name]
ms)
     ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtComprehension [ Prop -> Prop
pFin Prop
n' ]
     ([Match], Map Name (Located Prop), Prop)
-> InferM ([Match], Map Name (Located Prop), Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match
m1 Match -> [Match] -> [Match]
forall a. a -> [a] -> [a]
: [Match]
ms', (Located Prop -> Located Prop -> Located Prop)
-> Name
-> Located Prop
-> Map Name (Located Prop)
-> Map Name (Located Prop)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\Located Prop
_ Located Prop
old -> Located Prop
old) Name
x Located Prop
t Map Name (Located Prop)
ds, Prop -> Prop -> Prop
tMul Prop
n Prop
n')

{- | @inferBinds isTopLevel isRec binds@ performs inference for a
strongly-connected component of 'P.Bind's.
If any of the members of the recursive group are already marked
as monomorphic, then we don't do generalization.
If @isTopLevel@ is true,
any bindings without type signatures will be generalized. If it is
false, and the mono-binds flag is enabled, no bindings without type
signatures will be generalized, but bindings with signatures will
be unaffected.

-}

inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
isRec [Bind Name]
binds =
  do -- when mono-binds is enabled, and we're not checking top-level
     -- declarations, mark all bindings lacking signatures as monomorphic
     Bool
monoBinds <- InferM Bool
getMonoBinds
     let ([Bind Name]
sigs,[Bind Name]
noSigs) = (Bind Name -> Bool) -> [Bind Name] -> ([Bind Name], [Bind Name])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Schema Name) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Schema Name) -> Bool)
-> (Bind Name -> Maybe (Schema Name)) -> Bind Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind Name -> Maybe (Schema Name)
forall name. Bind name -> Maybe (Schema name)
P.bSignature) [Bind Name]
binds
         monos :: [Bind Name]
monos         = [Bind Name]
sigs [Bind Name] -> [Bind Name] -> [Bind Name]
forall a. [a] -> [a] -> [a]
++ [ Bind Name
b { P.bMono = True } | Bind Name
b <- [Bind Name]
noSigs ]
         binds' :: [Bind Name]
binds' | (Bind Name -> Bool) -> [Bind Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bind Name -> Bool
forall name. Bind name -> Bool
P.bMono [Bind Name]
binds           = [Bind Name]
monos
                | Bool
monoBinds Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isTopLevel = [Bind Name]
monos
                | Bool
otherwise                   = [Bind Name]
binds

         check :: Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap =
        {- Guess type is here, because while we check user supplied signatures
           we may generate additional constraints. For example, `x - y` would
           generate an additional constraint `x >= y`. -}
           do ([(Name, VarType)]
newEnv,[Either (InferM Decl) (InferM Decl)]
todos) <- [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Name, VarType), Either (InferM Decl) (InferM Decl))]
 -> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)]))
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
-> InferM ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
forall a b. (a -> b) -> InferM a -> InferM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Bind Name
 -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl)))
-> [Bind Name]
-> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
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 (Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType Map Name Expr
exprMap) [Bind Name]
binds'
              let otherEnv :: [(Name, VarType)]
otherEnv = ((Name, VarType) -> Bool) -> [(Name, VarType)] -> [(Name, VarType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, VarType) -> Bool
forall {a}. (a, VarType) -> Bool
isExt [(Name, VarType)]
newEnv

              let ([InferM Decl]
sigsAndMonos,[InferM Decl]
noSigGen) = [Either (InferM Decl) (InferM Decl)]
-> ([InferM Decl], [InferM Decl])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (InferM Decl) (InferM Decl)]
todos

              let prepGen :: InferM ([Decl], [Goal])
prepGen = InferM [Decl] -> InferM ([Decl], [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
                          (InferM [Decl] -> InferM ([Decl], [Goal]))
-> InferM [Decl] -> InferM ([Decl], [Goal])
forall a b. (a -> b) -> a -> b
$ do [Decl]
bs <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [InferM Decl]
noSigGen
                               InferM ()
simplifyAllConstraints
                               [Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
bs

              if Bool
isRec
                then
                  -- First we check the bindings with no signatures
                  -- that need to be generalized.
                  do ([Decl]
bs1,[Goal]
cs) <- [(Name, VarType)]
-> InferM ([Decl], [Goal]) -> InferM ([Decl], [Goal])
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv InferM ([Decl], [Goal])
prepGen

                     -- We add these to the environment, so their fvs are
                     -- not generalized.
                     [Decl]
genCs <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
otherEnv ([Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs)

                     -- Then we do all the rest,
                     -- using the newly inferred poly types.
                     let newEnv' :: [(Name, VarType)]
newEnv' = (Decl -> (Name, VarType)) -> [Decl] -> [(Name, VarType)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, VarType)
toExt [Decl]
bs1 [(Name, VarType)] -> [(Name, VarType)] -> [(Name, VarType)]
forall a. [a] -> [a] -> [a]
++ [(Name, VarType)]
otherEnv
                     [Decl]
done <- [(Name, VarType)] -> InferM [Decl] -> InferM [Decl]
forall a. [(Name, VarType)] -> InferM a -> InferM a
withVarTypes [(Name, VarType)]
newEnv' ([InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [InferM Decl]
sigsAndMonos)
                     ([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)

                else
                  do [Decl]
done      <- [InferM Decl] -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [InferM Decl]
sigsAndMonos
                     ([Decl]
bs1, [Goal]
cs) <- InferM ([Decl], [Goal])
prepGen
                     [Decl]
genCs     <- [Decl] -> [Goal] -> InferM [Decl]
generalize [Decl]
bs1 [Goal]
cs
                     ([Decl], [Decl]) -> InferM ([Decl], [Decl])
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
done,[Decl]
genCs)

     Bool -> [Bind Name] -> [Bind Name] -> InferM ()
checkNumericConstraintGuardsOK Bool
isTopLevel [Bind Name]
sigs [Bind Name]
noSigs

     rec
       let exprMap :: Map Name Expr
exprMap = [(Name, Expr)] -> Map Name Expr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Decl -> (Name, Expr)) -> [Decl] -> [(Name, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> (Name, Expr)
monoUse [Decl]
genBs)
       ([Decl]
doneBs, [Decl]
genBs) <- Map Name Expr -> InferM ([Decl], [Decl])
check Map Name Expr
exprMap

     InferM ()
simplifyAllConstraints

     [Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl]
doneBs [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
genBs)

  where
  toExt :: Decl -> (Name, VarType)
toExt Decl
d = (Decl -> Name
dName Decl
d, Schema -> VarType
ExtVar (Decl -> Schema
dSignature Decl
d))
  isExt :: (a, VarType) -> Bool
isExt (a
_,VarType
y) = case VarType
y of
                  ExtVar Schema
_ -> Bool
True
                  VarType
_        -> Bool
False

  monoUse :: Decl -> (Name, Expr)
monoUse Decl
d = (Name
x, Expr
withQs)
    where
    x :: Name
x  = Decl -> Name
dName Decl
d
    as :: [TParam]
as = Schema -> [TParam]
sVars (Decl -> Schema
dSignature Decl
d)
    qs :: [Prop]
qs = Schema -> [Prop]
sProps (Decl -> Schema
dSignature Decl
d)

    appT :: Expr -> TParam -> Expr
appT Expr
e TParam
a = Expr -> Prop -> Expr
ETApp Expr
e (TVar -> Prop
TVar (TParam -> TVar
tpVar TParam
a))
    appP :: Expr -> p -> Expr
appP Expr
e p
_ = Expr -> Expr
EProofApp Expr
e

    withTys :: Expr
withTys  = (Expr -> TParam -> Expr) -> Expr -> [TParam] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> TParam -> Expr
appT (Name -> Expr
EVar Name
x) [TParam]
as
    withQs :: Expr
withQs   = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Prop -> Expr
forall {p}. Expr -> p -> Expr
appP Expr
withTys  [Prop]
qs


{-
Here we also check that:
  * Numeric constraint guards appear only at the top level
  * All definitions in a recursive groups with numberic constraint guards
    have signatures

The reason is to avoid interference between local constraints coming
from the guards and type inference.  It might be possible to
relex these requirements, but this requires some more careful thought on
the interaction between the two, and the effects on pricniple types.
-}
checkNumericConstraintGuardsOK ::
  Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()
checkNumericConstraintGuardsOK :: Bool -> [Bind Name] -> [Bind Name] -> InferM ()
checkNumericConstraintGuardsOK Bool
isTopLevel [Bind Name]
haveSig [Bind Name]
noSig =
  do Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
isTopLevel
            ((Bind Name -> InferM ()) -> [Bind Name] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
NestedConstraintGuard) [Bind Name]
withGuards)
     Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bind Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bind Name]
withGuards)
            ((Bind Name -> InferM ()) -> [Bind Name] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
DeclarationRequiresSignatureCtrGrd) [Bind Name]
noSig)
  where
  mkErr :: (Ident -> Error) -> Bind Name -> InferM ()
mkErr Ident -> Error
f Bind Name
b =
    do let nm :: Located Name
nm = Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b
       Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
nm) (Error -> InferM ()
recordError (Ident -> Error
f (Name -> Ident
nameIdent (Located Name -> Name
forall a. Located a -> a
thing Located Name
nm))))

  withGuards :: [Bind Name]
withGuards = (Bind Name -> Bool) -> [Bind Name] -> [Bind Name]
forall a. (a -> Bool) -> [a] -> [a]
filter Bind Name -> Bool
forall name. Bind name -> Bool
hasConstraintGuards [Bind Name]
haveSig
  -- When desugaring constraint guards we check that they have signatures,
  -- so no need to look at noSig

  hasConstraintGuards :: Bind name -> Bool
hasConstraintGuards Bind name
b =
    case Bind name -> Maybe (BindImpl name)
forall name. Bind name -> Maybe (BindImpl name)
P.bindImpl Bind name
b of
      Just (P.DPropGuards {}) -> Bool
True
      Maybe (BindImpl name)
_                       -> Bool
False



{- | Come up with a type for recursive calls to a function, and decide
     how we are going to be checking the binding.
     Returns: (Name, type or schema, computation to check binding)

     The `exprMap` is a thunk where we can lookup the final expressions
     and we should be careful not to force it.
-}
guessType :: Map Name Expr -> P.Bind Name ->
              InferM ( (Name, VarType)
                     , Either (InferM Decl)    -- no generalization
                              (InferM Decl)    -- generalize these
                     )
guessType :: Map Name Expr
-> Bind Name
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
guessType Map Name Expr
exprMap b :: Bind Name
b@(P.Bind { Bool
[Pattern Name]
[Pragma]
Maybe Text
Maybe Fixity
Maybe (Schema Name)
Located Name
Located (BindDef Name)
ExportType
bMono :: forall name. Bind name -> Bool
bName :: forall name. Bind name -> Located name
bSignature :: forall name. Bind name -> Maybe (Schema name)
bName :: Located Name
bParams :: [Pattern Name]
bDef :: Located (BindDef Name)
bSignature :: Maybe (Schema Name)
bInfix :: Bool
bFixity :: Maybe Fixity
bPragmas :: [Pragma]
bMono :: Bool
bDoc :: Maybe Text
bExport :: ExportType
bParams :: forall name. Bind name -> [Pattern name]
bDef :: forall name. Bind name -> Located (BindDef name)
bInfix :: forall name. Bind name -> Bool
bFixity :: forall name. Bind name -> Maybe Fixity
bPragmas :: forall name. Bind name -> [Pragma]
bDoc :: forall name. Bind name -> Maybe Text
bExport :: forall name. Bind name -> ExportType
.. }) =
  case Maybe (Schema Name)
bSignature of

    Just Schema Name
s ->
      do let wildOk :: AllowWildCards
wildOk = case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing Located (BindDef Name)
bDef of
                        P.DForeign {}                   -> AllowWildCards
NoWildCards
                        BindDef Name
P.DPrim                         -> AllowWildCards
NoWildCards
                        P.DImpl BindImpl Name
i -> case BindImpl Name
i of
                                       P.DExpr {}       -> AllowWildCards
AllowWildCards
                                       P.DPropGuards {} -> AllowWildCards
NoWildCards
         (Schema, [Goal])
s1 <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
wildOk Schema Name
s
         ((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar ((Schema, [Goal]) -> Schema
forall a b. (a, b) -> a
fst (Schema, [Goal])
s1)), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Schema, [Goal])
s1))

    Maybe (Schema Name)
Nothing
      | Bool
bMono ->
         do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
            let schema :: Schema
schema = [TParam] -> [Prop] -> Prop -> Schema
Forall [] [] Prop
t
            ((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Schema -> VarType
ExtVar Schema
schema), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. a -> Either a b
Left (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))

      | Bool
otherwise ->

        do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Name -> TypeSource
DefinitionOf Name
name) Kind
KType
           let noWay :: a
noWay = String -> [String] -> a
forall a. String -> [String] -> a
tcPanic String
"guessType" [ String
"Missing expression for:" ,
                                                                Name -> String
forall a. Show a => a -> String
show Name
name ]
               expr :: Expr
expr  = Expr -> Name -> Map Name Expr -> Expr
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Expr
forall {a}. a
noWay Name
name Map Name Expr
exprMap

           ((Name, VarType), Either (InferM Decl) (InferM Decl))
-> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
name, Expr -> Prop -> VarType
CurSCC Expr
expr Prop
t), InferM Decl -> Either (InferM Decl) (InferM Decl)
forall a b. b -> Either a b
Right (Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t))
  where
  name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing Located Name
bName



{- | The inputs should be declarations with monomorphic types
(i.e., of the form `Forall [] [] t`). -}
generalize :: [Decl] -> [Goal] -> InferM [Decl]

{- This may happen because we have monomorphic bindings.
In this case we may get some goal, due to the monomorphic bindings,
but the group of components is empty. -}
generalize :: [Decl] -> [Goal] -> InferM [Decl]
generalize [] [Goal]
gs0 =
  do [Goal] -> InferM ()
addGoals [Goal]
gs0
     [Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return []


generalize [Decl]
bs0 [Goal]
gs0 =
  do {- First, we apply the accumulating substitution to the goals
        and the inferred types, to ensure that we have the most up
        to date information. -}
     [Goal]
gs <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
gs0
     [Decl]
bs <- [Decl] -> (Decl -> InferM Decl) -> InferM [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Decl]
bs0 ((Decl -> InferM Decl) -> InferM [Decl])
-> (Decl -> InferM Decl) -> InferM [Decl]
forall a b. (a -> b) -> a -> b
$ \Decl
b -> do Schema
s <- Schema -> InferM Schema
forall t. TVars t => t -> InferM t
applySubst (Decl -> Schema
dSignature Decl
b)
                               Decl -> InferM Decl
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
b { dSignature = s }

     -- Next, we figure out which of the free variables need to be generalized
     -- Variables apearing in the types of monomorphic bindings should
     -- not be generalizedr.
     let goalFVS :: Goal -> Set TVar
goalFVS Goal
g  = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Prop -> Set TVar) -> Prop -> Set TVar
forall a b. (a -> b) -> a -> b
$ Goal -> Prop
goal Goal
g
         inGoals :: Set TVar
inGoals    = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Goal -> Set TVar) -> [Goal] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Set TVar
goalFVS [Goal]
gs
         inSigs :: Set TVar
inSigs     = (TVar -> Bool) -> Set TVar -> Set TVar
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TVar -> Bool
isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
forall a b. (a -> b) -> a -> b
$ [Schema] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Schema] -> Set TVar) -> [Schema] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (Decl -> Schema) -> [Decl] -> [Schema]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Schema
dSignature [Decl]
bs
         candidates :: Set TVar
candidates = (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TVar
inGoals Set TVar
inSigs)

     Set TVar
asmpVs <- InferM (Set TVar)
varsWithAsmps

     let gen0 :: Set TVar
gen0          = Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
candidates Set TVar
asmpVs
         stays :: Goal -> Bool
stays Goal
g       = (TVar -> Bool) -> [TVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
gen0) ([TVar] -> Bool) -> [TVar] -> Bool
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> Set TVar -> [TVar]
forall a b. (a -> b) -> a -> b
$ Goal -> Set TVar
goalFVS Goal
g
         ([Goal]
here0,[Goal]
later) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Goal -> Bool
stays [Goal]
gs
     [Goal] -> InferM ()
addGoals [Goal]
later   -- these ones we keep around for to solve later

     let maybeAmbig :: [TVar]
maybeAmbig = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
gen0 Set TVar
inSigs)

     {- See if we might be able to default some of the potentially ambiguous
        variables using the constraints that will be part of the newly
        generalized schema.  -}
     let ([TVar]
as0,[Goal]
here1,Subst
defSu,[Warning]
ws,[Error]
errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
defaultAndSimplify [TVar]
maybeAmbig [Goal]
here0

     Subst -> InferM ()
extendSubst Subst
defSu
     (Warning -> InferM ()) -> [Warning] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Warning -> InferM ()
recordWarning [Warning]
ws
     (Error -> InferM ()) -> [Error] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Error -> InferM ()
recordError [Error]
errs
     let here :: [Prop]
here = (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal [Goal]
here1


     {- This is the variables we'll be generalizing:
          * any ones that survived the defaulting
          * and vars in the inferred types that do not appear anywhere else. -}
     let as :: [TVar]
as   = (TVar -> TVar -> Ordering) -> [TVar] -> [TVar]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy TVar -> TVar -> Ordering
forall {t} {t}. (HasKind t, HasKind t) => t -> t -> Ordering
numFst
              ([TVar] -> [TVar]) -> [TVar] -> [TVar]
forall a b. (a -> b) -> a -> b
$ [TVar]
as0 [TVar] -> [TVar] -> [TVar]
forall a. [a] -> [a] -> [a]
++ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TVar
inSigs Set TVar
asmpVs)
         asPs :: [TParam]
asPs = [ TParam { tpUnique :: Int
tpUnique = Int
x
                         , tpKind :: Kind
tpKind   = Kind
k
                         , tpFlav :: TPFlavor
tpFlav   = TPFlavor
TPUnifyVar
                         , tpInfo :: TVarInfo
tpInfo   = TVarInfo
i
                         }
                | TVFree Int
x Kind
k Set TParam
_ TVarInfo
i <- [TVar]
as
                ]

     {- Finally, we replace free variables with bound ones, and fix-up
        the definitions as needed to reflect that we are now working
        with polymorphic things. For example, apply each occurrence to the
        type parameters. -}
     Subst
totSu <- InferM Subst
getSubst
     let
         su :: Subst
su     = [(TVar, Prop)] -> Subst
listSubst ([TVar] -> [Prop] -> [(TVar, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TVar]
as ((TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
asPs)) Subst -> Subst -> Subst
@@ Subst
totSu
         qs :: [Prop]
qs     = (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Prop -> [Prop]
pSplitAnd (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Prop]
here

         genE :: Expr -> Expr
genE Expr
e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e) [Prop]
qs) [TParam]
asPs
         genB :: Decl -> Decl
genB Decl
d = Decl
d { dDefinition = case dDefinition d of
                                      DExpr Expr
e       -> Expr -> DeclDef
DExpr (Expr -> Expr
genE Expr
e)
                                      DeclDef
DPrim         -> DeclDef
DPrim
                                      DForeign FFIFunType
t Maybe Expr
me -> FFIFunType -> Maybe Expr -> DeclDef
DForeign FFIFunType
t (Expr -> Expr
genE (Expr -> Expr) -> Maybe Expr -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Expr
me)
                    , dSignature  = Forall asPs qs
                                  $ apSubst su $ sType $ dSignature d
                    }

     [Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Decl -> Decl) -> [Decl] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
genB [Decl]
bs)

  where
  numFst :: t -> t -> Ordering
numFst t
x t
y = case (t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
x, t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
y) of
                 (Kind
KNum, Kind
KNum) -> Ordering
EQ
                 (Kind
KNum, Kind
_)    -> Ordering
LT
                 (Kind
_,Kind
KNum)     -> Ordering
GT
                 (Kind, Kind)
_            -> Ordering
EQ

-- | Check a monomorphic binding.
checkMonoB :: P.Bind Name -> Type -> InferM Decl
checkMonoB :: Bind Name -> Prop -> InferM Decl
checkMonoB Bind Name
b Prop
t =
  Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
forall a b. (a -> b) -> a -> b
$
  case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of

    BindDef Name
P.DPrim -> String -> [String] -> InferM Decl
forall a. HasCallStack => String -> [String] -> a
panic String
"checkMonoB" [String
"Primitive with no signature?"]

    P.DForeign Maybe (BindImpl Name)
_ -> String -> [String] -> InferM Decl
forall a. HasCallStack => String -> [String] -> a
panic String
"checkMonoB" [String
"Foreign with no signature?"]

    P.DImpl BindImpl Name
i ->
      case BindImpl Name
i of

        P.DExpr Expr Name
e ->
          do let nm :: Name
nm = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
             let tGoal :: TypeWithSource
tGoal = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t (Name -> TypeSource
DefinitionOf Name
nm) (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b)
             Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (Maybe Name -> Int -> FunDesc Name
forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) Int
0) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e TypeWithSource
tGoal
             let f :: Name
f = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
             Decl -> InferM Decl
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Decl { dName :: Name
dName = Name
f
                         , dSignature :: Schema
dSignature = [TParam] -> [Prop] -> Prop -> Schema
Forall [] [] Prop
t
                         , dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e1
                         , dPragmas :: [Pragma]
dPragmas = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
                         , dInfix :: Bool
dInfix = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
                         , dFixity :: Maybe Fixity
dFixity = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
                         , dDoc :: Maybe Text
dDoc = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
                         }

        P.DPropGuards [PropGuardCase Name]
_ ->
          String -> [String] -> InferM Decl
forall a. String -> [String] -> a
tcPanic String
"checkMonoB"
            [ String
"Used constraint guards without a signature at "
            , Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Located Name -> Doc) -> Located Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located Name -> Doc
forall a. PP a => a -> Doc
pp (Located Name -> String) -> Located Name -> String
forall a b. (a -> b) -> a -> b
$ Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b ]

-- XXX: Do we really need to do the defaulting business in two different places?
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
checkSigB Bind Name
b (Forall [TParam]
as [Prop]
asmps0 Prop
t0, [Goal]
validSchema) =
  case Located (BindDef Name) -> BindDef Name
forall a. Located a -> a
thing (Bind Name -> Located (BindDef Name)
forall name. Bind name -> Located (BindDef name)
P.bDef Bind Name
b) of

    -- XXX what should we do with validSchema in this case?
    BindDef Name
P.DPrim ->
      Decl -> InferM Decl
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
        { dName :: Name
dName       = Name
name
        , dSignature :: Schema
dSignature  = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps0 Prop
t0
        , dDefinition :: DeclDef
dDefinition = DeclDef
DPrim
        , dPragmas :: [Pragma]
dPragmas    = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
        , dInfix :: Bool
dInfix      = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
        , dFixity :: Maybe Fixity
dFixity     = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
        , dDoc :: Maybe Text
dDoc        = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
        }

    P.DForeign Maybe (BindImpl Name)
mi -> do
      ([Prop]
asmps, Prop
t, Maybe Expr
me) <-
        case Maybe (BindImpl Name)
mi of
          Just BindImpl Name
i -> (Expr -> Maybe Expr)
-> ([Prop], Prop, Expr) -> ([Prop], Prop, Maybe Expr)
forall a b. (a -> b) -> ([Prop], Prop, a) -> ([Prop], Prop, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Maybe Expr
forall a. a -> Maybe a
Just (([Prop], Prop, Expr) -> ([Prop], Prop, Maybe Expr))
-> InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindImpl Name -> InferM ([Prop], Prop, Expr)
checkImpl BindImpl Name
i
          Maybe (BindImpl Name)
Nothing -> ([Prop], Prop, Maybe Expr) -> InferM ([Prop], Prop, Maybe Expr)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Prop]
asmps0, Prop
t0, Maybe Expr
forall a. Maybe a
Nothing)
      let loc :: Maybe Range
loc = Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b
          src :: TypeSource
src = Name -> TypeSource
DefinitionOf Name
name
      Maybe Range -> InferM Decl -> InferM Decl
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb Maybe Range
loc do
        -- Ensure all type params are of kind #
        [TParam] -> (TParam -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TParam]
as \TParam
a ->
          Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TParam -> Kind
tpKind TParam
a Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KNum) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
            Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
loc (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ TypeSource -> TParam -> Kind -> Error
UnsupportedFFIKind TypeSource
src TParam
a (Kind -> Error) -> Kind -> Error
forall a b. (a -> b) -> a -> b
$ TParam -> Kind
tpKind TParam
a
        [TParam] -> InferM Decl -> InferM Decl
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as do
          FFIFunType
ffiFunType <-
            case Schema -> Either FFITypeError ([Prop], FFIFunType)
toFFIFunType ([TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps Prop
t) of
              Right ([Prop]
props, FFIFunType
ffiFunType) -> FFIFunType
ffiFunType FFIFunType -> InferM Subst -> InferM FFIFunType
forall a b. a -> InferM b -> InferM a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
                [Goal]
ffiGoals <- (Prop -> InferM Goal) -> [Prop] -> InferM [Goal]
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 (ConstraintSource -> Prop -> InferM Goal
newGoal (Name -> ConstraintSource
CtFFI Name
name)) [Prop]
props
                Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
True (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name) [TParam]
as [Prop]
asmps ([Goal] -> InferM Subst) -> [Goal] -> InferM Subst
forall a b. (a -> b) -> a -> b
$
                  [Goal]
validSchema [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
ffiGoals
              Left FFITypeError
err -> do
                Maybe Range -> Error -> InferM ()
recordErrorLoc Maybe Range
loc (Error -> InferM ()) -> Error -> InferM ()
forall a b. (a -> b) -> a -> b
$ TypeSource -> FFITypeError -> Error
UnsupportedFFIType TypeSource
src FFITypeError
err
                -- Just a placeholder type
                FFIFunType -> InferM FFIFunType
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FFIFunType
                  { ffiTParams :: [TParam]
ffiTParams = [TParam]
as, ffiArgTypes :: [FFIType]
ffiArgTypes = []
                  , ffiRetType :: FFIType
ffiRetType = [FFIType] -> FFIType
FFITuple [] }
          Decl -> InferM Decl
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl { dName :: Name
dName       = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
                    , dSignature :: Schema
dSignature  = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps Prop
t
                    , dDefinition :: DeclDef
dDefinition = FFIFunType -> Maybe Expr -> DeclDef
DForeign FFIFunType
ffiFunType Maybe Expr
me
                    , dPragmas :: [Pragma]
dPragmas    = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
                    , dInfix :: Bool
dInfix      = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
                    , dFixity :: Maybe Fixity
dFixity     = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
                    , dDoc :: Maybe Text
dDoc        = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
                    }

    P.DImpl BindImpl Name
i -> do
      ([Prop]
asmps, Prop
t, Expr
expr) <- BindImpl Name -> InferM ([Prop], Prop, Expr)
checkImpl BindImpl Name
i
      Decl -> InferM Decl
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Decl
        { dName :: Name
dName       = Name
name
        , dSignature :: Schema
dSignature  = [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
asmps Prop
t
        , dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
expr
        , dPragmas :: [Pragma]
dPragmas    = Bind Name -> [Pragma]
forall name. Bind name -> [Pragma]
P.bPragmas Bind Name
b
        , dInfix :: Bool
dInfix      = Bind Name -> Bool
forall name. Bind name -> Bool
P.bInfix Bind Name
b
        , dFixity :: Maybe Fixity
dFixity     = Bind Name -> Maybe Fixity
forall name. Bind name -> Maybe Fixity
P.bFixity Bind Name
b
        , dDoc :: Maybe Text
dDoc        = Bind Name -> Maybe Text
forall name. Bind name -> Maybe Text
P.bDoc Bind Name
b
        }

  where

    name :: Name
name = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)

    checkImpl :: P.BindImpl Name -> InferM ([Prop], Type, Expr)
    checkImpl :: BindImpl Name -> InferM ([Prop], Prop, Expr)
checkImpl BindImpl Name
i =
      Maybe Range
-> InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a. Maybe Range -> InferM a -> InferM a
inRangeMb (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b) (InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr))
-> InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a b. (a -> b) -> a -> b
$
      [TParam]
-> InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a. [TParam] -> InferM a -> InferM a
withTParams [TParam]
as (InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr))
-> InferM ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a b. (a -> b) -> a -> b
$
      case BindImpl Name
i of

        P.DExpr Expr Name
e0 -> do
          (Prop
t, [Prop]
asmps, Expr
e2) <- [Prop] -> [Prop] -> Expr Name -> InferM (Prop, [Prop], Expr)
checkBindDefExpr [] [Prop]
asmps0 Expr Name
e0
          ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [Prop]
asmps
               , Prop
t
               , (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs Expr
e2 [Prop]
asmps) [TParam]
as
               )

        P.DPropGuards [PropGuardCase Name]
cases0 -> do
          [Prop]
asmps1 <- [Prop] -> InferM [Prop]
applySubstPreds [Prop]
asmps0
          Prop
t1     <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
t0
          [([Prop], Expr)]
cases1 <- (PropGuardCase Name -> InferM ([Prop], Expr))
-> [PropGuardCase Name] -> InferM [([Prop], Expr)]
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 PropGuardCase Name -> InferM ([Prop], Expr)
checkPropGuardCase [PropGuardCase Name]
cases0

          Bool
exh <- Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b) [TParam]
as [Prop]
asmps1 ((([Prop], Expr) -> [Prop]) -> [([Prop], Expr)] -> [[Prop]]
forall a b. (a -> b) -> [a] -> [b]
map ([Prop], Expr) -> [Prop]
forall a b. (a, b) -> a
fst [([Prop], Expr)]
cases1)
          Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exh (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
              -- didn't prove exhaustive i.e. none of the guarding props
              -- necessarily hold
              Warning -> InferM ()
recordWarning (Name -> Warning
NonExhaustivePropGuards Name
name)

          ([Prop], Prop, Expr) -> InferM ([Prop], Prop, Expr)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [Prop]
asmps1
               , Prop
t1
               , (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs
                   ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs
                     ([([Prop], Expr)] -> Prop -> Expr
EPropGuards [([Prop], Expr)]
cases1 Prop
t1)
                   [Prop]
asmps1)
                 [TParam]
as
               )

    checkBindDefExpr ::
      [Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)
    checkBindDefExpr :: [Prop] -> [Prop] -> Expr Name -> InferM (Prop, [Prop], Expr)
checkBindDefExpr [Prop]
asmpsSign [Prop]
asmps1 Expr Name
e0 = do

      (Expr
e1,[Goal]
cs0) <- InferM Expr -> InferM (Expr, [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals (InferM Expr -> InferM (Expr, [Goal]))
-> InferM Expr -> InferM (Expr, [Goal])
forall a b. (a -> b) -> a -> b
$ do
        let nm :: Name
nm = Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b)
            tGoal :: TypeWithSource
tGoal = Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
t0 (Name -> TypeSource
DefinitionOf Name
nm) (Bind Name -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Bind Name
b)
        Expr
e1 <- FunDesc Name
-> [Pattern Name] -> Expr Name -> TypeWithSource -> InferM Expr
checkFun (Maybe Name -> Int -> FunDesc Name
forall n. Maybe n -> Int -> FunDesc n
P.FunDesc (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) Int
0) (Bind Name -> [Pattern Name]
forall name. Bind name -> [Pattern name]
P.bParams Bind Name
b) Expr Name
e0 TypeWithSource
tGoal
        [Goal] -> InferM ()
addGoals [Goal]
validSchema
        () <- InferM ()
simplifyAllConstraints  -- XXX: using `asmps` also?
        Expr -> InferM Expr
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e1
      [Prop]
asmps2 <- [Prop] -> InferM [Prop]
applySubstPreds [Prop]
asmps1
      [Goal]
cs     <- [Goal] -> InferM [Goal]
applySubstGoals [Goal]
cs0

      let findKeep :: Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set a
vs [a]
keep [(a, Set a)]
todo =
            let stays :: (a, Set a) -> Bool
stays (a
_,Set a
cvs)    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Bool
forall a. Set a -> Bool
Set.null (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
vs Set a
cvs
                ([(a, Set a)]
yes,[(a, Set a)]
perhaps)    = ((a, Set a) -> Bool)
-> [(a, Set a)] -> ([(a, Set a)], [(a, Set a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a, Set a) -> Bool
forall {a}. (a, Set a) -> Bool
stays [(a, Set a)]
todo
                ([a]
stayPs,[Set a]
newVars) = [(a, Set a)] -> ([a], [Set a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, Set a)]
yes
            in case [a]
stayPs of
                [] -> ([a]
keep,((a, Set a) -> a) -> [(a, Set a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Set a) -> a
forall a b. (a, b) -> a
fst [(a, Set a)]
todo)
                [a]
_  -> Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep ([Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set a
vsSet a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
:[Set a]
newVars)) ([a]
stayPs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
keep) [(a, Set a)]
perhaps

      let -- if a goal mentions any of these variables, we'll commit to
          -- solving it now.
          stickyVars :: Set TVar
stickyVars = [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Prop] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Prop]
asmps2
          ([Goal]
stay,[Goal]
leave) = Set TVar -> [Goal] -> [(Goal, Set TVar)] -> ([Goal], [Goal])
forall {a} {a}. Ord a => Set a -> [a] -> [(a, Set a)] -> ([a], [a])
findKeep Set TVar
stickyVars []
                              [ (Goal
c, Goal -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Goal
c) | Goal
c <- [Goal]
cs ]

      [Goal] -> InferM ()
addGoals [Goal]
leave

      -- includes asmpsSign for the sake of implication, but doesn't actually
      -- include them in the resulting asmps
      Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
True (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (Bind Name -> Located Name
forall name. Bind name -> Located name
P.bName Bind Name
b))) [TParam]
as ([Prop]
asmpsSign [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
asmps2) [Goal]
stay
      Subst -> InferM ()
extendSubst Subst
su

      let asmps :: [Prop]
asmps  = (Prop -> [Prop]) -> [Prop] -> [Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [Prop]
pSplitAnd (Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Prop]
asmps2)
      Prop
t      <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
t0
      Expr
e2     <- Expr -> InferM Expr
forall t. TVars t => t -> InferM t
applySubst Expr
e1

      (Prop, [Prop], Expr) -> InferM (Prop, [Prop], Expr)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop
t, [Prop]
asmps, Expr
e2)



{- |
Given a DPropGuards of the form

@
f : {...} A
f | (B1, B2) => ...
  | (C1, C2, C2) => ...
@

we check that it is exhaustive by trying to prove the following
implications:

@
  A /\ ~B1 => C1 /\ C2 /\ C3
  A /\ ~B2 => C1 /\ C2 /\ C3
@

The implications were derive by the following general algorithm:
- Find that @(C1, C2, C3)@ is the guard that has the most conjuncts, so we
  will keep it on the RHS of the generated implications in order to minimize
  the number of implications we need to check.
- Negate @(B1, B2)@ which yields @(~B1) \/ (~B2)@. This is a disjunction, so
  we need to consider a branch for each disjunct --- one branch gets the
  assumption @~B1@ and another branch gets the assumption @~B2@. Each
  branch's implications need to be proven independently.

-}
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive Located Name
name [TParam]
as [Prop]
asmps [[Prop]]
guards =
  case ([Prop] -> [Prop] -> Ordering) -> [[Prop]] -> [[Prop]]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [Prop] -> [Prop] -> Ordering
forall {t :: * -> *} {t :: * -> *} {a} {a}.
(Foldable t, Foldable t) =>
t a -> t a -> Ordering
cmpByLonger [[Prop]]
guards of
    [] -> Bool -> InferM Bool
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False -- XXX: we should check the asmps are unsatisfiable
    [Prop]
longest : [[Prop]]
rest -> [[Prop]] -> [Goal] -> InferM Bool
doGoals ([[Prop]] -> [[Prop]]
theAlts [[Prop]]
rest) ((Prop -> Goal) -> [Prop] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Goal
toGoal [Prop]
longest)

  where
  cmpByLonger :: t a -> t a -> Ordering
cmpByLonger t a
props1 t a
props2 = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
props2) (t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
props1)
                                          -- reversed, so that longets is first

  theAlts :: [[Prop]] -> [[Prop]]
  theAlts :: [[Prop]] -> [[Prop]]
theAlts = ([[Prop]] -> [Prop]) -> [[[Prop]]] -> [[Prop]]
forall a b. (a -> b) -> [a] -> [b]
map [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[Prop]]] -> [[Prop]])
-> ([[Prop]] -> [[[Prop]]]) -> [[Prop]] -> [[Prop]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[Prop]]] -> [[[Prop]]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([[[Prop]]] -> [[[Prop]]])
-> ([[Prop]] -> [[[Prop]]]) -> [[Prop]] -> [[[Prop]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Prop] -> [[Prop]]) -> [[Prop]] -> [[[Prop]]]
forall a b. (a -> b) -> [a] -> [b]
map [Prop] -> [[Prop]]
chooseNeg

  -- Choose one of the things to negate
  chooseNeg :: [Prop] -> [[Prop]]
chooseNeg [Prop]
ps =
    case [Prop]
ps of
      []     -> []
      Prop
p : [Prop]
qs -> (Prop -> [Prop]
pNegNumeric Prop
p [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
qs) [Prop] -> [[Prop]] -> [[Prop]]
forall a. a -> [a] -> [a]
: [ Prop
p Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
: [Prop]
alts | [Prop]
alts <- [Prop] -> [[Prop]]
chooseNeg [Prop]
qs ]



  -- Try to validate all cases
  doGoals :: [[Prop]] -> [Goal] -> InferM Bool
doGoals [[Prop]]
todo [Goal]
gs =
    case [[Prop]]
todo of
      []     -> Bool -> InferM Bool
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      [Prop]
alt : [[Prop]]
more ->
        do Bool
ok <- [Prop] -> [Goal] -> InferM Bool
canProve ([Prop]
asmps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
alt) [Goal]
gs
           if Bool
ok then [[Prop]] -> [Goal] -> InferM Bool
doGoals [[Prop]]
more [Goal]
gs
                 else Bool -> InferM Bool
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  toGoal :: Prop -> Goal
  toGoal :: Prop -> Goal
toGoal Prop
prop =
    Goal
      { goalSource :: ConstraintSource
goalSource = Name -> ConstraintSource
CtPropGuardsExhaustive (Located Name -> Name
forall a. Located a -> a
thing Located Name
name)
      , goalRange :: Range
goalRange  = Located Name -> Range
forall a. Located a -> Range
srcRange Located Name
name
      , goal :: Prop
goal       = Prop
prop
      }

  canProve :: [Prop] -> [Goal] -> InferM Bool
  canProve :: [Prop] -> [Goal] -> InferM Bool
canProve [Prop]
asmps' [Goal]
goals =
    Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
tryProveImplication (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing Located Name
name)) [TParam]
as [Prop]
asmps' [Goal]
goals

{- | This function does not validate anything---it just translates into
the type-checkd syntax.  The actual validation of the guard will happen
when the (automatically generated) function corresponding to the guard is
checked, assuming 'ExpandpropGuards' did its job correctly.

-}
checkPropGuardCase :: P.PropGuardCase Name -> InferM ([Prop],Expr)
checkPropGuardCase :: PropGuardCase Name -> InferM ([Prop], Expr)
checkPropGuardCase (P.PropGuardCase [Located (Prop Name)]
guards Expr Name
e0) =
  do [Prop]
ps <- [Located (Prop Name)] -> InferM [Prop]
checkPropGuards [Located (Prop Name)]
guards
     [Prop]
tys <- (Type Name -> InferM Prop) -> [Type Name] -> InferM [Prop]
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 (Type Name -> Maybe Kind -> InferM Prop
`checkType` Maybe Kind
forall a. Maybe a
Nothing) [Type Name]
ts
     let rhsTs :: Expr
rhsTs = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp                  (Expr Name -> Expr
getV Expr Name
eV) [Prop]
tys
         rhsPs :: Expr
rhsPs = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e Prop
_p -> Expr -> Expr
EProofApp Expr
e) Expr
rhsTs     [Prop]
ps
         rhs :: Expr
rhs   = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp                   Expr
rhsPs     ((Expr Name -> Expr) -> [Expr Name] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr Name -> Expr
getV [Expr Name]
es)
     ([Prop], Expr) -> InferM ([Prop], Expr)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Prop]
ps,Expr
rhs)

  where
  (Expr Name
e1,[Expr Name]
es) = Expr Name -> (Expr Name, [Expr Name])
forall n. Expr n -> (Expr n, [Expr n])
P.asEApps Expr Name
e0
  (Expr Name
eV,[Type Name]
ts) = case Expr Name
e1 of
              P.EAppT Expr Name
ex1 [TypeInst Name]
tis -> (Expr Name
ex1, (TypeInst Name -> Type Name) -> [TypeInst Name] -> [Type Name]
forall a b. (a -> b) -> [a] -> [b]
map TypeInst Name -> Type Name
forall {name}. TypeInst name -> Type name
getT [TypeInst Name]
tis)
              Expr Name
_               -> (Expr Name
e1, [])

  getV :: Expr Name -> Expr
getV Expr Name
ex =
    case Expr Name
ex of
      P.EVar Name
x -> Name -> Expr
EVar Name
x
      Expr Name
_        -> String -> Expr
forall {a}. String -> a
bad String
"Expression is not a variable."

  getT :: TypeInst name -> Type name
getT TypeInst name
ti =
    case TypeInst name
ti of
      P.PosInst Type name
t    -> Type name
t
      P.NamedInst {} -> String -> Type name
forall {a}. String -> a
bad String
"Unexpeceted NamedInst"

  bad :: String -> a
bad String
msg = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"checkPropGuardCase" [String
msg]

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

checkLocalDecls :: [P.Decl Name] -> InferM a -> InferM (a,[DeclGroup])
checkLocalDecls :: forall a. [Decl Name] -> InferM a -> InferM (a, [DeclGroup])
checkLocalDecls [Decl Name]
ds0 InferM a
k =
  do InferM ()
newLocalScope
     [Decl Name] -> (Decl Name -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Decl Name]
ds0 \Decl Name
d -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
False Decl Name
d Maybe Text
forall a. Maybe a
Nothing
     a
a <- InferM a
k
     ([DeclGroup]
ds,Map Name TySyn
_tySyns) <- InferM ([DeclGroup], Map Name TySyn)
endLocalScope
     (a, [DeclGroup]) -> InferM (a, [DeclGroup])
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a,[DeclGroup]
ds)



checkTopDecls :: [P.TopDecl Name] -> InferM ()
checkTopDecls :: [TopDecl Name] -> InferM ()
checkTopDecls = (TopDecl Name -> InferM ()) -> [TopDecl Name] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TopDecl Name -> InferM ()
checkTopDecl
  where
  checkTopDecl :: TopDecl Name -> InferM ()
checkTopDecl TopDecl Name
decl =
    case TopDecl Name
decl of
      P.Decl TopLevel (Decl Name)
tl -> Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
True (TopLevel (Decl Name) -> Decl Name
forall a. TopLevel a -> a
P.tlValue TopLevel (Decl Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (Decl Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Decl Name)
tl)

      P.TDNewtype TopLevel (Newtype Name)
tl ->
        do NominalType
t <- Newtype Name -> Maybe Text -> InferM NominalType
checkNewtype (TopLevel (Newtype Name) -> Newtype Name
forall a. TopLevel a -> a
P.tlValue TopLevel (Newtype Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (Newtype Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (Newtype Name)
tl)
           NominalType -> InferM ()
addNominal NominalType
t

      P.TDEnum TopLevel (EnumDecl Name)
tl ->
        do NominalType
t <- EnumDecl Name -> Maybe Text -> InferM NominalType
checkEnum (TopLevel (EnumDecl Name) -> EnumDecl Name
forall a. TopLevel a -> a
P.tlValue TopLevel (EnumDecl Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (EnumDecl Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (EnumDecl Name)
tl)
           NominalType -> InferM ()
addNominal NominalType
t

      P.DPrimType TopLevel (PrimType Name)
tl ->
        do NominalType
t <- PrimType Name -> Maybe Text -> InferM NominalType
checkPrimType (TopLevel (PrimType Name) -> PrimType Name
forall a. TopLevel a -> a
P.tlValue TopLevel (PrimType Name)
tl) (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (PrimType Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (PrimType Name)
tl)
           NominalType -> InferM ()
addNominal NominalType
t


      P.DInterfaceConstraint Maybe Text
_ Located [Prop Name]
cs ->
        Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located [Prop Name] -> Range
forall a. Located a -> Range
srcRange Located [Prop Name]
cs)
        do [Located Prop]
cs1 <- [Located (Prop Name)] -> InferM [Located Prop]
checkParameterConstraints [ Located [Prop Name]
cs { thing = c } | Prop Name
c <- Located [Prop Name] -> [Prop Name]
forall a. Located a -> a
thing Located [Prop Name]
cs ]
           [Located Prop] -> InferM ()
addParameterConstraints [Located Prop]
cs1

      P.DModule TopLevel (NestedModule Name)
tl ->
         InferM () -> InferM ()
forall a. InferM a -> InferM a
selectorScope
         case ModuleG Name Name -> ModuleDefinition Name
forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef ModuleG Name Name
m of

           P.NormalModule [TopDecl Name]
ds ->
             do Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> InferM ()
newSubmoduleScope (Located Name -> Name
forall a. Located a -> a
thing (ModuleG Name Name -> Located Name
forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m))
                                  (Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (NestedModule Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl)
                                  ([TopDecl Name] -> ExportSpec Name
forall name. Ord name => [TopDecl name] -> ExportSpec name
P.exportedDecls [TopDecl Name]
ds)
                                  (ModuleG Name Name -> NamingEnv
forall mname name. ModuleG mname name -> NamingEnv
P.mInScope ModuleG Name Name
m)
                [TopDecl Name] -> InferM ()
checkTopDecls [TopDecl Name]
ds
                InferM ()
proveModuleTopLevel
                InferM ()
endSubmodule

           P.FunctorInstance Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst ->
             do let doc :: Maybe Text
doc = Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (NestedModule Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl
                Maybe TCTopEntity
_ <- Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> ModuleInstance Name
-> NamingEnv
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst
                  (Name -> ImpName Name
forall name. name -> ImpName name
P.ImpNested (Name -> ImpName Name) -> Located Name -> Located (ImpName Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleG Name Name -> Located Name
forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m) Located (ImpName Name)
f ModuleInstanceArgs Name
as ModuleInstance Name
inst (ModuleG Name Name -> NamingEnv
forall mname name. ModuleG mname name -> NamingEnv
P.mInScope ModuleG Name Name
m) Maybe Text
doc
                () -> InferM ()
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

           P.InterfaceModule Signature Name
sig ->
              do let doc :: Maybe Text
doc = Located Text -> Text
forall a. Located a -> a
P.thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevel (NestedModule Name) -> Maybe (Located Text)
forall a. TopLevel a -> Maybe (Located Text)
P.tlDoc TopLevel (NestedModule Name)
tl
                 Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located Name -> Range
forall a. Located a -> Range
srcRange (ModuleG Name Name -> Located Name
forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m))
                   do Name -> Maybe Text -> InferM ()
newSignatureScope (Located Name -> Name
forall a. Located a -> a
thing (ModuleG Name Name -> Located Name
forall mname name. ModuleG mname name -> Located mname
P.mName ModuleG Name Name
m)) Maybe Text
doc
                      Signature Name -> InferM ()
checkSignature Signature Name
sig
                      InferM ()
endSignature


        where P.NestedModule ModuleG Name Name
m = TopLevel (NestedModule Name) -> NestedModule Name
forall a. TopLevel a -> a
P.tlValue TopLevel (NestedModule Name)
tl

      P.DModParam ModParam Name
p ->
        Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located (ImpName Name) -> Range
forall a. Located a -> Range
srcRange (ModParam Name -> Located (ImpName Name)
forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p))
        do let binds :: ModuleInstance Name
binds = ModParam Name -> ModuleInstance Name
forall name. ModParam name -> Map name name
P.mpRenaming ModParam Name
p
               suMap :: ModuleInstance Name
suMap = [(Name, Name)] -> ModuleInstance Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
y,Name
x) | (Name
x,Name
y) <- ModuleInstance Name -> [(Name, Name)]
forall k a. Map k a -> [(k, a)]
Map.toList ModuleInstance Name
binds ]
               actualName :: Name -> Name
actualName Name
x = Name -> Name -> ModuleInstance Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x ModuleInstance Name
suMap

           ModParamNames
ips <- ImpName Name -> InferM ModParamNames
lookupSignature (Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing (ModParam Name -> Located (ImpName Name)
forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p))
           let actualTys :: [ModTParam]
actualTys  = [ (Name -> Name) -> ModTParam -> ModTParam
forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName ModTParam
mp
                            | ModTParam
mp <- Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ips) ]
               actualTS :: [TySyn]
actualTS   = [ (Name -> Name) -> TySyn -> TySyn
forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName TySyn
ts
                            | TySyn
ts <- Map Name TySyn -> [TySyn]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
ips)
                            ]
               actualCtrs :: [Located Prop]
actualCtrs = [ (Name -> Name) -> Located Prop -> Located Prop
forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName Located Prop
prop
                            | Located Prop
prop <- ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
ips ]
               actualVals :: [ModVParam]
actualVals = [ (Name -> Name) -> ModVParam -> ModVParam
forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames Name -> Name
actualName ModVParam
vp
                            | ModVParam
vp <- Map Name ModVParam -> [ModVParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ips) ]

               param :: ModParam
param =
                 ModParam
                   { mpName :: Ident
mpName = ModParam Name -> Ident
forall name. ModParam name -> Ident
P.mpName ModParam Name
p
                   , mpIface :: ImpName Name
mpIface = Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing (ModParam Name -> Located (ImpName Name)
forall name. ModParam name -> Located (ImpName name)
P.mpSignature ModParam Name
p)
                   , mpQual :: Maybe ModName
mpQual = ModParam Name -> Maybe ModName
forall name. ModParam name -> Maybe ModName
P.mpAs ModParam Name
p
                   , mpParameters :: ModParamNames
mpParameters =
                        ModParamNames
                          { mpnTypes :: Map Name ModTParam
mpnTypes = [(Name, ModTParam)] -> Map Name ModTParam
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ModTParam -> Name
mtpName ModTParam
tp, ModTParam
tp)
                                                    | ModTParam
tp <- [ModTParam]
actualTys ]
                          , mpnTySyn :: Map Name TySyn
mpnTySyn = [(Name, TySyn)] -> Map Name TySyn
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TySyn -> Name
tsName TySyn
ts, TySyn
ts)
                                                    | TySyn
ts <- [TySyn]
actualTS ]
                          , mpnConstraints :: [Located Prop]
mpnConstraints = [Located Prop]
actualCtrs
                          , mpnFuns :: Map Name ModVParam
mpnFuns = [(Name, ModVParam)] -> Map Name ModVParam
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ModVParam -> Name
mvpName ModVParam
vp, ModVParam
vp)
                                                   | ModVParam
vp <- [ModVParam]
actualVals ]
                          , mpnDoc :: Maybe Text
mpnDoc = Located Text -> Text
forall a. Located a -> a
thing (Located Text -> Text) -> Maybe (Located Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModParam Name -> Maybe (Located Text)
forall name. ModParam name -> Maybe (Located Text)
P.mpDoc ModParam Name
p
                          }
                   }

           (ModTParam -> InferM ()) -> [ModTParam] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ModTParam -> InferM ()
addParamType [ModTParam]
actualTys
           [Located Prop] -> InferM ()
addParameterConstraints [Located Prop]
actualCtrs
           (ModVParam -> InferM ()) -> [ModVParam] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ModVParam -> InferM ()
addParamFun [ModVParam]
actualVals
           (TySyn -> InferM ()) -> [TySyn] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TySyn -> InferM ()
addTySyn [TySyn]
actualTS
           ModParam -> InferM ()
addModParam ModParam
param

      P.DImport {}        -> () -> InferM ()
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      P.Include {}        -> String -> InferM ()
forall {a}. String -> a
bad String
"Include"
      P.DParamDecl {}     -> String -> InferM ()
forall {a}. String -> a
bad String
"DParamDecl"


  bad :: String -> a
bad String
x = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"checkTopDecl" [ String
x ]


checkSignature :: P.Signature Name -> InferM ()
checkSignature :: Signature Name -> InferM ()
checkSignature Signature Name
sig =
  do [ParameterType Name]
-> (ParameterType Name -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Signature Name -> [ParameterType Name]
forall name. Signature name -> [ParameterType name]
P.sigTypeParams Signature Name
sig) \ParameterType Name
pt ->
       ModTParam -> InferM ()
addParamType (ModTParam -> InferM ()) -> InferM ModTParam -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ParameterType Name -> InferM ModTParam
checkParameterType ParameterType Name
pt

     (SigDecl Name -> InferM ()) -> [SigDecl Name] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SigDecl Name -> InferM ()
checkSigDecl (Signature Name -> [SigDecl Name]
forall name. Signature name -> [SigDecl name]
P.sigDecls Signature Name
sig)

     [Located Prop] -> InferM ()
addParameterConstraints ([Located Prop] -> InferM ()) -> InferM [Located Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        [Located (Prop Name)] -> InferM [Located Prop]
checkParameterConstraints (Signature Name -> [Located (Prop Name)]
forall name. Signature name -> [Located (Prop name)]
P.sigConstraints Signature Name
sig)

     [ParameterFun Name]
-> (ParameterFun Name -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Signature Name -> [ParameterFun Name]
forall name. Signature name -> [ParameterFun name]
P.sigFunParams Signature Name
sig) \ParameterFun Name
f ->
       ModVParam -> InferM ()
addParamFun (ModVParam -> InferM ()) -> InferM ModVParam -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
f

     InferM ()
proveModuleTopLevel

checkSigDecl :: P.SigDecl Name -> InferM ()
checkSigDecl :: SigDecl Name -> InferM ()
checkSigDecl SigDecl Name
decl =
  case SigDecl Name
decl of

    P.SigTySyn TySyn Name
ts Maybe Text
mbD ->
      TySyn -> InferM ()
addTySyn (TySyn -> InferM ()) -> InferM TySyn -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TySyn Name -> Maybe Text -> InferM TySyn
checkTySyn TySyn Name
ts Maybe Text
mbD

    P.SigPropSyn PropSyn Name
ps Maybe Text
mbD ->
      TySyn -> InferM ()
addTySyn (TySyn -> InferM ()) -> InferM TySyn -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PropSyn Name -> Maybe Text -> InferM TySyn
checkPropSyn PropSyn Name
ps Maybe Text
mbD



checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
checkDecl :: Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d Maybe Text
mbDoc =
  case Decl Name
d of

    P.DBind Bind Name
c ->
      do ~[Decl
b] <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
False [Bind Name
c]
         DeclGroup -> InferM ()
addDecls (Decl -> DeclGroup
NonRecursive Decl
b)

    P.DRec [Bind Name]
bs ->
      do [Decl]
bs1 <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
isTopLevel Bool
True [Bind Name]
bs
         DeclGroup -> InferM ()
addDecls ([Decl] -> DeclGroup
Recursive [Decl]
bs1)

    P.DType TySyn Name
t ->
      do TySyn
t1 <- TySyn Name -> Maybe Text -> InferM TySyn
checkTySyn TySyn Name
t Maybe Text
mbDoc
         TySyn -> InferM ()
addTySyn TySyn
t1

    P.DProp PropSyn Name
t ->
      do TySyn
t1 <- PropSyn Name -> Maybe Text -> InferM TySyn
checkPropSyn PropSyn Name
t Maybe Text
mbDoc
         TySyn -> InferM ()
addTySyn TySyn
t1

    P.DLocated Decl Name
d' Range
r -> Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange Range
r (Bool -> Decl Name -> Maybe Text -> InferM ()
checkDecl Bool
isTopLevel Decl Name
d' Maybe Text
mbDoc)

    P.DSignature {} -> String -> InferM ()
forall {a}. String -> a
bad String
"DSignature"
    P.DFixity {}    -> String -> InferM ()
forall {a}. String -> a
bad String
"DFixity"
    P.DPragma {}    -> String -> InferM ()
forall {a}. String -> a
bad String
"DPragma"
    P.DPatBind {}   -> String -> InferM ()
forall {a}. String -> a
bad String
"DPatBind"

  where
  bad :: String -> a
bad String
x = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"checkDecl" [String
x]


checkParameterFun :: P.ParameterFun Name -> InferM ModVParam
checkParameterFun :: ParameterFun Name -> InferM ModVParam
checkParameterFun ParameterFun Name
x =
  do (Schema
s,[Goal]
gs) <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
checkSchema AllowWildCards
NoWildCards (ParameterFun Name -> Schema Name
forall name. ParameterFun name -> Schema name
P.pfSchema ParameterFun Name
x)
     Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
False (Name -> Maybe Name
forall a. a -> Maybe a
Just (Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)))
                                  (Schema -> [TParam]
sVars Schema
s) (Schema -> [Prop]
sProps Schema
s) [Goal]
gs
     Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Subst -> Bool
isEmptySubst Subst
su) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
       String -> [String] -> InferM ()
forall a. HasCallStack => String -> [String] -> a
panic String
"checkParameterFun" [String
"Subst not empty??"]
     let n :: Name
n = Located Name -> Name
forall a. Located a -> a
thing (ParameterFun Name -> Located Name
forall name. ParameterFun name -> Located name
P.pfName ParameterFun Name
x)
     ModVParam -> InferM ModVParam
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ModVParam { mvpName :: Name
mvpName = Name
n
                      , mvpType :: Schema
mvpType = Schema
s
                      , mvpDoc :: Maybe Text
mvpDoc  = ParameterFun Name -> Maybe Text
forall name. ParameterFun name -> Maybe Text
P.pfDoc ParameterFun Name
x
                      , mvpFixity :: Maybe Fixity
mvpFixity = ParameterFun Name -> Maybe Fixity
forall name. ParameterFun name -> Maybe Fixity
P.pfFixity ParameterFun Name
x
                      }



tcPanic :: String -> [String] -> a
tcPanic :: forall a. String -> [String] -> a
tcPanic String
l [String]
msg = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic (String
"[TypeCheck] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l) [String]
msg