    -- |
    -- 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 ViewPatterns #-}
    {-# LANGUAGE RecursiveDo #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Infer
      ( checkE
      , checkSigB
      , inferModule
      , inferBinds
      , inferDs
      )
    where

    import           Cryptol.ModuleSystem.Name (asPrim,lookupPrimDecl,nameLoc)
    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,
                                            checkParameterType,
                                            checkPrimType,
                                            checkParameterConstraints)
    import           Cryptol.TypeCheck.Instantiate
    import           Cryptol.TypeCheck.Depends
    import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
    import           Cryptol.TypeCheck.Solver.InfNat(genLog)
    import           Cryptol.Utils.Ident
    import           Cryptol.Utils.Panic(panic)
    import           Cryptol.Utils.PP

    import qualified Data.Map as Map
    import           Data.Map (Map)
    import qualified Data.Set as Set
    import           Data.List(foldl',sortBy)
    import           Data.Either(partitionEithers)
    import           Data.Maybe(mapMaybe,isJust, fromMaybe)
    import           Data.List(partition,find)
    import           Data.Graph(SCC(..))
    import           Data.Traversable(forM)
    import           Control.Monad(zipWithM,unless,foldM)

    inferModule :: P.Module Name -> InferM Module
    inferModule :: Module Name -> InferM Module
    inferModule m :: Module Name
    m =
      [TopDecl Name] -> ([DeclGroup] -> InferM Module) -> InferM Module
    forall d a.
    FromDecl d =>
    [d] -> ([DeclGroup] -> InferM a) -> InferM a
    inferDs (Module Name -> [TopDecl Name]
    forall name. Module name -> [TopDecl name]
    P.mDecls Module Name
    m) (([DeclGroup] -> InferM Module) -> InferM Module)
    -> ([DeclGroup] -> InferM Module) -> InferM Module
    forall a b. (a -> b) -> a -> b
    $ \ds1 :: [DeclGroup]
    ds1 ->
        do InferM ()
    proveModuleTopLevel
           Map Name (DefLoc, TySyn)
    ts <- InferM (Map Name (DefLoc, TySyn))
    getTSyns
           Map Name (DefLoc, Newtype)
    nts <- InferM (Map Name (DefLoc, Newtype))
    getNewtypes
           Map Name (DefLoc, AbstractType)
    ats <- InferM (Map Name (DefLoc, AbstractType))
    getAbstractTypes
           Map Name ModTParam
    pTs <- InferM (Map Name ModTParam)
    getParamTypes
           [Located Prop]
    pCs <- InferM [Located Prop]
    getParamConstraints
           Map Name ModVParam
    pFuns <- InferM (Map Name ModVParam)
    getParamFuns
           Module -> InferM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WModule :: ModName
    -> ExportSpec Name
    -> [Import]
    -> Map Name TySyn
    -> Map Name Newtype
    -> Map Name AbstractType
    -> Map Name ModTParam
    -> [Located Prop]
    -> Map Name ModVParam
    -> [DeclGroup]
    -> Module
    Module { mName :: ModName
    mName      = Located ModName -> ModName
    forall a. Located a -> a
    thing (Module Name -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module Name
    m)
                         , mExports :: ExportSpec Name
    mExports   = Module Name -> ExportSpec Name
    forall name. Ord name => Module name -> ExportSpec name
    P.modExports Module Name
    m
                         , mImports :: [Import]
    mImports   = (Located Import -> Import) -> [Located Import] -> [Import]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Import -> Import
    forall a. Located a -> a
    thing (Module Name -> [Located Import]
    forall name. Module name -> [Located Import]
    P.mImports Module Name
    m)
                         , mTySyns :: Map Name TySyn
    mTySyns    = ((DefLoc, TySyn) -> Maybe TySyn)
    -> Map Name (DefLoc, TySyn) -> Map Name TySyn
    forall a b k. (a -> Maybe b) -> Map k a -> Map k b
    Map.mapMaybe (DefLoc, TySyn) -> Maybe TySyn
    forall a. (DefLoc, a) -> Maybe a
    onlyLocal Map Name (DefLoc, TySyn)
    ts
                         , mNewtypes :: Map Name Newtype
    mNewtypes  = ((DefLoc, Newtype) -> Maybe Newtype)
    -> Map Name (DefLoc, Newtype) -> Map Name Newtype
    forall a b k. (a -> Maybe b) -> Map k a -> Map k b
    Map.mapMaybe (DefLoc, Newtype) -> Maybe Newtype
    forall a. (DefLoc, a) -> Maybe a
    onlyLocal Map Name (DefLoc, Newtype)
    nts
                         , mPrimTypes :: Map Name AbstractType
    mPrimTypes = ((DefLoc, AbstractType) -> Maybe AbstractType)
    -> Map Name (DefLoc, AbstractType) -> Map Name AbstractType
    forall a b k. (a -> Maybe b) -> Map k a -> Map k b
    Map.mapMaybe (DefLoc, AbstractType) -> Maybe AbstractType
    forall a. (DefLoc, a) -> Maybe a
    onlyLocal Map Name (DefLoc, AbstractType)
    ats
                         , mParamTypes :: Map Name ModTParam
    mParamTypes = Map Name ModTParam
    pTs
                         , mParamConstraints :: [Located Prop]
    mParamConstraints = [Located Prop]
    pCs
                         , mParamFuns :: Map Name ModVParam
    mParamFuns = Map Name ModVParam
    pFuns
                         , mDecls :: [DeclGroup]
    mDecls     = [DeclGroup]
    ds1
                         }
      where
      onlyLocal :: (DefLoc, a) -> Maybe a
    onlyLocal (IsLocal, x :: a
    x)    = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x
      onlyLocal (IsExternal, _) = Maybe a
    forall a. Maybe a
    Nothing

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

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

    desugarLiteral :: Bool -> P.Literal -> InferM (P.Expr Name)
    desugarLiteral :: Bool -> Literal -> InferM (Expr Name)
    desugarLiteral fixDec :: Bool
    fixDec lit :: Literal
    lit =
      do Range
    l <- InferM Range
    curRange
         Expr Name
    numberPrim <- String -> InferM (Expr Name)
    mkPrim "number"
         let named :: (String, Type name) -> TypeInst name
    named (x :: String
    x,y :: Type name
    y)  = Named (Type name) -> TypeInst name
    forall name. Named (Type name) -> TypeInst name
    P.NamedInst
                            Named :: forall a. Located Ident -> a -> Named a
    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 fs :: [(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 n :: 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 (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 num :: Integer
    num info :: 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
    $ [ ("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 n :: Int
    n    -> [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits (1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n)) ]
               P.OctLit n :: Int
    n    -> [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits (3 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n)) ]
               P.HexLit n :: Int
    n    -> [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits (4 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n)) ]
               P.CharLit     -> [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits (8 :: Integer)) ]
               P.DecLit
                | Bool
    fixDec     -> if Integer
    num Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
                                  then [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits 0)]
                                  else case Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    num 2 of
                                         Just (x :: Integer
    x,_) -> [ ("rep", Integer -> Type Name
    forall n. Integer -> Type n
    tBits (Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + 1)) ]
                                         _          -> []
                | Bool
    otherwise  -> [ ]
               P.PolyLit _n :: Int
    _n  -> [ ("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.ECString s :: 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 (Integer -> NumInfo -> Literal
    P.ECNum (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c))
                                NumInfo
    P.CharLit) | 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 8) Type Name
    forall n. Type n
    P.TBit))

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

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

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

        P.EAppT e :: Expr Name
    e fs :: [TypeInst Name]
    fs -> Expr Name -> [TypeArg] -> Prop -> 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) Prop
    tGoal

        -- Here is an example of why this might be useful:
        -- f ` { x = T } where type T = ...
        P.EWhere e :: Expr Name
    e ds :: [Decl Name]
    ds ->
          [Decl Name] -> ([DeclGroup] -> InferM Expr) -> InferM Expr
    forall d a.
    FromDecl d =>
    [d] -> ([DeclGroup] -> InferM a) -> InferM a
    inferDs [Decl Name]
    ds (([DeclGroup] -> InferM Expr) -> InferM Expr)
    -> ([DeclGroup] -> InferM Expr) -> InferM Expr
    forall a b. (a -> b) -> a -> b
    $ \ds1 :: [DeclGroup]
    ds1 -> do Expr
    e1 <- Expr Name -> [TypeArg] -> Prop -> InferM Expr
    appTys Expr Name
    e [TypeArg]
    ts Prop
    tGoal
                                  Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> [DeclGroup] -> Expr
    EWhere Expr
    e1 [DeclGroup]
    ds1)
             -- XXX: Is there a scoping issue here?  I think not, but check.

        P.ELocated e :: Expr Name
    e r :: Range
    r ->
          Range -> InferM Expr -> InferM Expr
    forall a. Range -> InferM a -> InferM a
    inRange Range
    r (Expr Name -> [TypeArg] -> Prop -> InferM Expr
    appTys Expr Name
    e [TypeArg]
    ts Prop
    tGoal)

        P.ENeg        {} -> InferM Expr
    mono
        P.EComplement {} -> InferM Expr
    mono
        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.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.EParens e :: Expr Name
    e       -> Expr Name -> [TypeArg] -> Prop -> InferM Expr
    appTys Expr Name
    e [TypeArg]
    ts Prop
    tGoal
        P.EInfix a :: Expr Name
    a op :: Located Name
    op _ b :: Expr Name
    b -> Expr Name -> [TypeArg] -> Prop -> 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 Prop
    tGoal

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

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

      (named :: [TypeArg]
    named,pos :: [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 ty :: Type Name
    ty k :: 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 -> Type -> InferM Expr
    checkE :: Expr Name -> Prop -> InferM Expr
    checkE expr :: Expr Name
    expr tGoal :: Prop
    tGoal =
      case Expr Name
    expr of
        P.EVar x :: Name
    x ->
          do VarType
    res <- Name -> InferM VarType
    lookupVar Name
    x
             (e' :: Expr
    e',t :: Prop
    t) <- case VarType
    res of
                         ExtVar s :: Schema
    s   -> Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
    instantiateWith Name
    x (Name -> Expr
    EVar Name
    x) Schema
    s []
                         CurSCC e :: Expr
    e t :: Prop
    t -> (Expr, Prop) -> InferM (Expr, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr
    e, Prop
    t)

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

        P.ENeg e :: Expr Name
    e ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "negate"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.EComplement e :: Expr Name
    e ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "complement"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.EGenerate e :: Expr Name
    e ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "generate"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.ELit l :: Literal
    l@(P.ECNum _ P.DecLit) ->
          do Expr Name
    e <- Bool -> Literal -> InferM (Expr Name)
    desugarLiteral Bool
    False 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 :: Maybe (Located Ident) -> MaybeCheckedType -> TypeArg
    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 "rep"))
                               , tyArgType :: MaybeCheckedType
    tyArgType = Prop -> MaybeCheckedType
    Checked Prop
    tGoal
                               }
             Expr Name -> [TypeArg] -> Prop -> InferM Expr
    appTys Expr Name
    e [TypeArg
    arg] Prop
    tGoal

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

        P.ETuple es :: [Expr Name]
    es ->
          do [Prop]
    etys <- Int -> Prop -> InferM [Prop]
    expectTuple ([Expr Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Expr Name]
    es) Prop
    tGoal
             [Expr]
    es'  <- (Expr Name -> Prop -> InferM Expr)
    -> [Expr Name] -> [Prop] -> InferM [Expr]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Expr Name -> Prop -> InferM Expr
    checkE [Expr Name]
    es [Prop]
    etys
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Expr] -> Expr
    ETuple [Expr]
    es')

        P.ERecord fs :: [Named (Expr Name)]
    fs ->
          do (ns :: [Ident]
    ns,es :: [Expr Name]
    es,ts :: [Prop]
    ts) <- [(Ident, Expr Name, Prop)] -> ([Ident], [Expr Name], [Prop])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 ([(Ident, Expr Name, Prop)] -> ([Ident], [Expr Name], [Prop]))
    -> InferM [(Ident, Expr Name, Prop)]
    -> InferM ([Ident], [Expr Name], [Prop])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` [Named (Expr Name)] -> Prop -> InferM [(Ident, Expr Name, Prop)]
    forall a. [Named a] -> Prop -> InferM [(Ident, a, Prop)]
    expectRec [Named (Expr Name)]
    fs Prop
    tGoal
             [Expr]
    es' <- (Expr Name -> Prop -> InferM Expr)
    -> [Expr Name] -> [Prop] -> InferM [Expr]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Expr Name -> Prop -> InferM Expr
    checkE [Expr Name]
    es [Prop]
    ts
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Ident, Expr)] -> Expr
    ERec ([Ident] -> [Expr] -> [(Ident, Expr)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    ns [Expr]
    es'))

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

        P.ESel e :: Expr Name
    e l :: Selector
    l ->
          do Prop
    t <- TVarSource -> Kind -> InferM Prop
    newType (Selector -> TVarSource
    selSrc Selector
    l) Kind
    KType
             Expr
    e' <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    t
             HasGoalSln
    f <- Selector -> Prop -> Prop -> InferM HasGoalSln
    newHasGoal Selector
    l Prop
    t Prop
    tGoal
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HasGoalSln -> Expr -> Expr
    hasDoSelect HasGoalSln
    f Expr
    e')

        P.EList [] ->
          do (len :: Prop
    len,a :: Prop
    a) <- Prop -> InferM (Prop, Prop)
    expectSeq Prop
    tGoal
             Int -> Prop -> InferM ()
    expectFin 0 Prop
    len
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Expr] -> Prop -> Expr
    EList [] Prop
    a)

        P.EList es :: [Expr Name]
    es ->
          do (len :: Prop
    len,a :: Prop
    a) <- Prop -> InferM (Prop, Prop)
    expectSeq Prop
    tGoal
             Int -> Prop -> InferM ()
    expectFin ([Expr Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Expr Name]
    es) Prop
    len
             [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)
    mapM (Expr Name -> Prop -> InferM Expr
    `checkE` Prop
    a) [Expr Name]
    es
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Expr] -> Prop -> Expr
    EList [Expr]
    es' Prop
    a)

        P.EFromTo t1 :: Type Name
    t1 mbt2 :: Maybe (Type Name)
    mbt2 t3 :: Type Name
    t3 mety :: Maybe (Type Name)
    mety ->
          do Range
    l <- InferM Range
    curRange
             let fs0 :: [(String, Type Name)]
    fs0 =
                   case Maybe (Type Name)
    mety of
                     Just ety :: Type Name
    ety -> [("a", Type Name
    ety)]
                     Nothing -> []
             let (c :: String
    c,fs :: [(String, Type Name)]
    fs) =
                   case Maybe (Type Name)
    mbt2 of
                     Nothing ->
                        ("fromTo", ("last", Type Name
    t3) (String, Type Name)
    -> [(String, Type Name)] -> [(String, Type Name)]
    forall a. a -> [a] -> [a]
    : [(String, Type Name)]
    fs0)
                     Just t2 :: Type Name
    t2 ->
                        ("fromThenTo", ("next",Type Name
    t2) (String, Type Name)
    -> [(String, Type Name)] -> [(String, Type Name)]
    forall a. a -> [a] -> [a]
    : ("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 Named :: forall a. Located Ident -> a -> Named a
    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 }
                      | (x :: String
    x,y :: Type Name
    y) <- ("first",Type Name
    t1) (String, Type Name)
    -> [(String, Type Name)] -> [(String, Type Name)]
    forall a. a -> [a] -> [a]
    : [(String, Type Name)]
    fs
                      ]

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

        P.EInfFrom e1 :: Expr Name
    e1 Nothing ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "infFrom"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.EInfFrom e1 :: Expr Name
    e1 (Just e2 :: Expr Name
    e2) ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "infFromThen"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.EComp e :: Expr Name
    e mss :: [[Match Name]]
    mss ->
          do (mss' :: [[Match]]
    mss', dss :: [Map Name (Located Prop)]
    dss, ts :: [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 (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 [ 1 .. ] [[Match Name]]
    mss
             (len :: Prop
    len,a :: Prop
    a) <- Prop -> InferM (Prop, Prop)
    expectSeq Prop
    tGoal

             ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtComprehension ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Prop -> Prop -> InferM [Prop]
    unify Prop
    len (Prop -> InferM [Prop]) -> InferM Prop -> InferM [Prop]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Prop] -> InferM Prop
    smallest [Prop]
    ts

             Map Name (Located Prop)
    ds     <- [Map Name (Located Prop)] -> InferM (Map Name (Located Prop))
    forall a. [Map Name (Located a)] -> InferM (Map Name (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 -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    a)
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Prop -> Expr -> [[Match]] -> Expr
    EComp Prop
    len Prop
    a Expr
    e' [[Match]]
    mss')

        P.EAppT e :: Expr Name
    e fs :: [TypeInst Name]
    fs -> Expr Name -> [TypeArg] -> Prop -> 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) Prop
    tGoal

        P.EApp fun :: Expr Name
    fun@(Expr Name -> Expr Name
    forall t. AddLoc t => t -> t
    dropLoc -> P.EApp (Expr Name -> Expr Name
    forall t. AddLoc t => t -> t
    dropLoc -> P.EVar c :: Name
    c) _)
               arg :: Expr Name
    arg@(Expr Name -> Expr Name
    forall t. AddLoc t => t -> t
    dropLoc -> P.ELit l :: Literal
    l)
          | Just n :: Ident
    n <- Name -> Maybe Ident
    asPrim Name
    c
          , Ident
    n Ident -> [Ident] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` (String -> Ident) -> [String] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> Ident
    packIdent [ "<<", ">>", "<<<", ">>>" , "@", "!" ] ->
            do Expr Name
    newArg <- do Expr Name
    l1 <- Bool -> Literal -> InferM (Expr Name)
    desugarLiteral Bool
    True Literal
    l
                            Expr Name -> InferM (Expr Name)
    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 Expr Name
    arg of
                                       P.ELocated _ pos :: Range
    pos -> Expr Name -> Range -> Expr Name
    forall n. Expr n -> Range -> Expr n
    P.ELocated Expr Name
    l1 Range
    pos
                                       _ -> Expr Name
    l1
               Expr Name -> Prop -> InferM Expr
    checkE (Expr Name -> Expr Name -> Expr Name
    forall n. Expr n -> Expr n -> Expr n
    P.EApp Expr Name
    fun Expr Name
    newArg) Prop
    tGoal

        P.EApp e1 :: Expr Name
    e1 e2 :: Expr Name
    e2 ->
          do Prop
    t1  <- TVarSource -> Kind -> InferM Prop
    newType (Maybe Int -> TVarSource
    TypeOfArg Maybe Int
    forall a. Maybe a
    Nothing) Kind
    KType
             Expr
    e1' <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e1 (Prop -> Prop -> Prop
    tFun Prop
    t1 Prop
    tGoal)
             Expr
    e2' <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e2 Prop
    t1
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Expr -> Expr
    EApp Expr
    e1' Expr
    e2')

        P.EIf e1 :: Expr Name
    e1 e2 :: Expr Name
    e2 e3 :: Expr Name
    e3 ->
          do Expr
    e1'      <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e1 Prop
    tBit
             Expr
    e2'      <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e2 Prop
    tGoal
             Expr
    e3'      <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e3 Prop
    tGoal
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Expr -> Expr -> Expr
    EIf Expr
    e1' Expr
    e2' Expr
    e3')

        P.EWhere e :: Expr Name
    e ds :: [Decl Name]
    ds ->
          [Decl Name] -> ([DeclGroup] -> InferM Expr) -> InferM Expr
    forall d a.
    FromDecl d =>
    [d] -> ([DeclGroup] -> InferM a) -> InferM a
    inferDs [Decl Name]
    ds (([DeclGroup] -> InferM Expr) -> InferM Expr)
    -> ([DeclGroup] -> InferM Expr) -> InferM Expr
    forall a b. (a -> b) -> a -> b
    $ \ds1 :: [DeclGroup]
    ds1 -> do Expr
    e1 <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tGoal
                                  Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> [DeclGroup] -> Expr
    EWhere Expr
    e1 [DeclGroup]
    ds1)

        P.ETyped e :: Expr Name
    e t :: Type Name
    t ->
          do Prop
    tSig <- Type Name -> Kind -> InferM Prop
    checkTypeOfKind Type Name
    t Kind
    KType
             Expr
    e'   <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tSig
             Prop -> Prop -> InferM ()
    checkHasType Prop
    tSig Prop
    tGoal
             Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e'

        P.ETypeVal t :: Type Name
    t ->
          do Range
    l <- InferM Range
    curRange
             Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "number"
             Expr Name -> Prop -> 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
                       Named :: forall a. Located Ident -> a -> Named a
    P.Named { name :: Located Ident
    name = Range -> Ident -> Located Ident
    forall a. Range -> a -> Located a
    Located Range
    l (String -> Ident
    packIdent "val")
                               , value :: Type Name
    value = Type Name
    t }]) Prop
    tGoal

        P.EFun ps :: [Pattern Name]
    ps e :: Expr Name
    e -> Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
    checkFun (String -> Doc
    text "anonymous function") [Pattern Name]
    ps Expr Name
    e Prop
    tGoal

        P.ELocated e :: Expr Name
    e r :: Range
    r  -> Range -> InferM Expr -> InferM Expr
    forall a. Range -> InferM a -> InferM a
    inRange Range
    r (Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tGoal)

        P.ESplit e :: Expr Name
    e ->
          do Expr Name
    prim <- String -> InferM (Expr Name)
    mkPrim "splitAt"
             Expr Name -> Prop -> 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) Prop
    tGoal

        P.EInfix a :: Expr Name
    a op :: Located Name
    op _ b :: Expr Name
    b -> Expr Name -> Prop -> 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) Prop
    tGoal

        P.EParens e :: Expr Name
    e -> Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tGoal

    selSrc :: P.Selector -> TVarSource
    selSrc :: Selector -> TVarSource
    selSrc l :: Selector
    l = case Selector
    l of
                 RecordSel la :: Ident
    la _ -> Ident -> TVarSource
    TypeOfRecordField Ident
    la
                 TupleSel n :: Int
    n _   -> Int -> TVarSource
    TypeOfTupleField Int
    n
                 ListSel _ _    -> TVarSource
    TypeOfSeqElement

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

        -- { _ | fs } ~~>  \r -> { r | fs }
        Nothing ->
          do Name
    r <- Ident -> InferM Name
    newParamName (String -> Ident
    packIdent "r")
             let p :: Pattern Name
    p  = Located Name -> Pattern Name
    forall n. Located n -> Pattern n
    P.PVar $WLocated :: forall a. Range -> a -> Located a
    Located { srcRange :: Range
    srcRange = Name -> Range
    nameLoc Name
    r, thing :: Name
    thing = Name
    r }
                 fe :: Expr Name
    fe = [Pattern Name] -> Expr Name -> Expr Name
    forall n. [Pattern n] -> Expr n -> Expr n
    P.EFun [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 -> Prop -> InferM Expr
    checkE Expr Name
    fe Prop
    tGoal

        Just e :: Expr Name
    e ->
          do Expr
    e1 <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tGoal
             (Expr -> UpdField Name -> InferM Expr)
    -> Expr -> [UpdField Name] -> InferM Expr
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM Expr -> UpdField Name -> InferM Expr
    doUpd Expr
    e1 [UpdField Name]
    fs

      where
      doUpd :: Expr -> UpdField Name -> InferM Expr
    doUpd e :: Expr
    e (P.UpdField how :: UpdHow
    how sels :: [Located Selector]
    sels v :: Expr Name
    v) =
        case [Located Selector]
    sels of
          [l :: Located Selector
    l] ->
            case UpdHow
    how of
              P.UpdSet ->
                do Prop
    ft <- TVarSource -> Kind -> InferM Prop
    newType (Selector -> TVarSource
    selSrc Selector
    s) Kind
    KType
                   Expr
    v1 <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    v Prop
    ft
                   HasGoalSln
    d  <- Selector -> Prop -> Prop -> InferM HasGoalSln
    newHasGoal Selector
    s Prop
    tGoal Prop
    ft
                   Expr -> InferM Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (HasGoalSln -> Expr -> Expr -> Expr
    hasDoSet HasGoalSln
    d Expr
    e Expr
    v1)
              P.UpdFun ->
                 do Prop
    ft <- TVarSource -> Kind -> InferM Prop
    newType (Selector -> TVarSource
    selSrc Selector
    s) Kind
    KType
                    Expr
    v1 <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    v (Prop -> Prop -> Prop
    tFun Prop
    ft Prop
    ft)
                    HasGoalSln
    d  <- Selector -> Prop -> Prop -> InferM HasGoalSln
    newHasGoal Selector
    s Prop
    tGoal Prop
    ft
                    Name
    tmp <- Ident -> InferM Name
    newParamName (String -> Ident
    packIdent "rf")
                    let e' :: Expr
    e' = Name -> Expr
    EVar Name
    tmp
                    Expr -> InferM Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> InferM Expr) -> Expr -> InferM Expr
    forall a b. (a -> b) -> a -> b
    $ 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
                              $WDecl :: Name
    -> Schema
    -> DeclDef
    -> [Pragma]
    -> Bool
    -> Maybe Fixity
    -> Maybe String
    -> Decl
    Decl { dName :: Name
    dName        = Name
    tmp
                                   , dSignature :: Schema
    dSignature   = Prop -> Schema
    tMono Prop
    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 String
    dDoc         = Maybe String
    forall a. Maybe a
    Nothing
                                   } ]

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

    expectSeq :: Type -> InferM (Type,Type)
    expectSeq :: Prop -> InferM (Prop, Prop)
    expectSeq ty :: Prop
    ty =
      case Prop
    ty of

        TUser _ _ ty' :: Prop
    ty' ->
             Prop -> InferM (Prop, Prop)
    expectSeq Prop
    ty'

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

        TVar _ ->
          do tys :: (Prop, Prop)
    tys@(a :: Prop
    a,b :: 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
    =<< Prop -> Prop -> InferM [Prop]
    unify Prop
    ty (Prop -> Prop -> Prop
    tSeq Prop
    a Prop
    b)
             (Prop, Prop) -> InferM (Prop, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop, Prop)
    tys

        _ ->
          do tys :: (Prop, Prop)
    tys@(a :: Prop
    a,b :: Prop
    b) <- InferM (Prop, Prop)
    genTys
             Error -> InferM ()
    recordError (Prop -> Prop -> Error
    TypeMismatch Prop
    ty (Prop -> Prop -> Prop
    tSeq Prop
    a Prop
    b))
             (Prop, Prop) -> InferM (Prop, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop, Prop)
    tys
      where
      genTys :: InferM (Prop, Prop)
    genTys =
        do Prop
    a <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    LenOfSeq Kind
    KNum
           Prop
    b <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    TypeOfSeqElement Kind
    KType
           (Prop, Prop) -> InferM (Prop, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop
    a,Prop
    b)

    expectTuple :: Int -> Type -> InferM [Type]
    expectTuple :: Int -> Prop -> InferM [Prop]
    expectTuple n :: Int
    n ty :: Prop
    ty =
      case Prop
    ty of

        TUser _ _ ty' :: Prop
    ty' ->
             Int -> Prop -> InferM [Prop]
    expectTuple Int
    n Prop
    ty'

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

        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
    =<< Prop -> Prop -> InferM [Prop]
    unify Prop
    ty ([Prop] -> Prop
    tTuple [Prop]
    tys)
             [Prop] -> InferM [Prop]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Prop]
    tys

        _ ->
          do [Prop]
    tys <- InferM [Prop]
    genTys
             Error -> InferM ()
    recordError (Prop -> Prop -> Error
    TypeMismatch Prop
    ty ([Prop] -> Prop
    tTuple [Prop]
    tys))
             [Prop] -> InferM [Prop]
    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 [ 0 .. Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1 ] ((Int -> InferM Prop) -> InferM [Prop])
    -> (Int -> InferM Prop) -> InferM [Prop]
    forall a b. (a -> b) -> a -> b
    $ \ i :: Int
    i -> TVarSource -> Kind -> InferM Prop
    newType (Int -> TVarSource
    TypeOfTupleField Int
    i) Kind
    KType

    expectRec :: [P.Named a] -> Type -> InferM [(Ident,a,Type)]
    expectRec :: [Named a] -> Prop -> InferM [(Ident, a, Prop)]
    expectRec fs :: [Named a]
    fs ty :: Prop
    ty =
      case Prop
    ty of

        TUser _ _ ty' :: Prop
    ty' ->
             [Named a] -> Prop -> InferM [(Ident, a, Prop)]
    forall a. [Named a] -> Prop -> InferM [(Ident, a, Prop)]
    expectRec [Named a]
    fs Prop
    ty'

        TRec ls :: [(Ident, Prop)]
    ls | Just tys :: [(Ident, a, Prop)]
    tys <- ((Ident, Prop) -> Maybe (Ident, a, Prop))
    -> [(Ident, Prop)] -> Maybe [(Ident, a, Prop)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Ident, Prop) -> Maybe (Ident, a, Prop)
    forall c. (Ident, c) -> Maybe (Ident, a, c)
    checkField [(Ident, Prop)]
    ls ->
             [(Ident, a, Prop)] -> InferM [(Ident, a, Prop)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Ident, a, Prop)]
    tys

        _ ->
          do (tys :: [(Ident, Prop)]
    tys,res :: [(Ident, a, Prop)]
    res) <- InferM ([(Ident, Prop)], [(Ident, a, Prop)])
    genTys
             case Prop
    ty of
               TVar TVFree{} -> do [Prop]
    ps <- Prop -> Prop -> InferM [Prop]
    unify Prop
    ty ([(Ident, Prop)] -> Prop
    TRec [(Ident, Prop)]
    tys)
                                   ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtExactType [Prop]
    ps
               _ -> Error -> InferM ()
    recordError (Prop -> Prop -> Error
    TypeMismatch Prop
    ty ([(Ident, Prop)] -> Prop
    TRec [(Ident, Prop)]
    tys))
             [(Ident, a, Prop)] -> InferM [(Ident, a, Prop)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Ident, a, Prop)]
    res

      where
      checkField :: (Ident, c) -> Maybe (Ident, a, c)
    checkField (n :: Ident
    n,t :: c
    t) =
        do Named a
    f <- (Named a -> Bool) -> [Named a] -> Maybe (Named a)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find (\f :: Named a
    f -> Located Ident -> Ident
    forall a. Located a -> a
    thing (Named a -> Located Ident
    forall a. Named a -> Located Ident
    P.name Named a
    f) Ident -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ident
    n) [Named a]
    fs
           (Ident, a, c) -> Maybe (Ident, a, c)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Located Ident -> Ident
    forall a. Located a -> a
    thing (Named a -> Located Ident
    forall a. Named a -> Located Ident
    P.name Named a
    f), Named a -> a
    forall a. Named a -> a
    P.value Named a
    f, c
    t)

      genTys :: InferM ([(Ident, Prop)], [(Ident, a, Prop)])
    genTys =
        do [(Ident, a, Prop)]
    res <- [Named a]
    -> (Named a -> InferM (Ident, a, Prop))
    -> InferM [(Ident, a, Prop)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Named a]
    fs ((Named a -> InferM (Ident, a, Prop)) -> InferM [(Ident, a, Prop)])
    -> (Named a -> InferM (Ident, a, Prop))
    -> InferM [(Ident, a, Prop)]
    forall a b. (a -> b) -> a -> b
    $ \ f :: Named a
    f ->
                 do let field :: Ident
    field = Located Ident -> Ident
    forall a. Located a -> a
    thing (Named a -> Located Ident
    forall a. Named a -> Located Ident
    P.name Named a
    f)
                    Prop
    t <- TVarSource -> Kind -> InferM Prop
    newType (Ident -> TVarSource
    TypeOfRecordField Ident
    field) Kind
    KType
                    (Ident, a, Prop) -> InferM (Ident, a, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ident
    field, Named a -> a
    forall a. Named a -> a
    P.value Named a
    f, Prop
    t)

           let (ls :: [Ident]
    ls,_,ts :: [Prop]
    ts) = [(Ident, a, Prop)] -> ([Ident], [a], [Prop])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 [(Ident, a, Prop)]
    res
           ([(Ident, Prop)], [(Ident, a, Prop)])
    -> InferM ([(Ident, Prop)], [(Ident, a, Prop)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Ident] -> [Prop] -> [(Ident, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    ls [Prop]
    ts, [(Ident, a, Prop)]
    res)

    expectFin :: Int -> Type -> InferM ()
    expectFin :: Int -> Prop -> InferM ()
    expectFin n :: Int
    n ty :: Prop
    ty =
      case Prop
    ty of

        TUser _ _ ty' :: Prop
    ty' ->
             Int -> Prop -> InferM ()
    expectFin Int
    n Prop
    ty'

        TCon (TC (TCNum n' :: 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 (m :: * -> *) a. Monad m => a -> m a
    return ()

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

    expectFun :: Int -> Type -> InferM ([Type],Type)
    expectFun :: Int -> Prop -> InferM ([Prop], Prop)
    expectFun  = [Prop] -> Int -> Prop -> InferM ([Prop], Prop)
    go []
      where

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

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

            TCon (TC TCFun) [a :: Prop
    a,b :: 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
    - 1) Prop
    b

            _ ->
              do [Prop]
    args <- Int -> InferM [Prop]
    genArgs Int
    arity
                 Prop
    res  <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    TypeOfRes Kind
    KType
                 case Prop
    ty of
                   TVar TVFree{} -> do [Prop]
    ps <- Prop -> Prop -> InferM [Prop]
    unify Prop
    ty ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
    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
                   _             -> Error -> InferM ()
    recordError (Prop -> Prop -> Error
    TypeMismatch Prop
    ty ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return ([Prop] -> [Prop]
    forall a. [a] -> [a]
    reverse [Prop]
    tys, Prop
    ty)

      genArgs :: Int -> InferM [Prop]
    genArgs arity :: 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 [ 1 .. Int
    arity ] ((Int -> InferM Prop) -> InferM [Prop])
    -> (Int -> InferM Prop) -> InferM [Prop]
    forall a b. (a -> b) -> a -> b
    $
                        \ ix :: Int
    ix -> TVarSource -> Kind -> InferM Prop
    newType (Maybe Int -> TVarSource
    TypeOfArg (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    ix)) Kind
    KType

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

    checkFun :: Doc -> [P.Pattern Name] -> P.Expr Name -> Type -> InferM Expr
    checkFun :: Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
    checkFun _    [] e :: Expr Name
    e tGoal :: Prop
    tGoal = Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tGoal
    checkFun desc :: Doc
    desc ps :: [Pattern Name]
    ps e :: Expr Name
    e tGoal :: Prop
    tGoal =
      InferM Expr -> InferM Expr
    forall a. InferM a -> InferM a
    inNewScope (InferM Expr -> InferM Expr) -> InferM Expr -> InferM Expr
    forall a b. (a -> b) -> a -> b
    $
      do let descs :: [Doc]
    descs = [ String -> Doc
    text "type of" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    n Doc -> Doc -> Doc
    <+> String -> Doc
    text "argument"
                         Doc -> Doc -> Doc
    <+> String -> Doc
    text "of" Doc -> Doc -> Doc
    <+> Doc
    desc | Int
    n <- [ 1 :: Int .. ] ]

         (tys :: [Prop]
    tys,tRes :: Prop
    tRes) <- Int -> Prop -> InferM ([Prop], Prop)
    expectFun ([Pattern Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Pattern Name]
    ps) Prop
    tGoal
         [Located Name]
    largs      <- [InferM (Located Name)] -> InferM [Located Name]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence ((Doc -> Pattern Name -> Prop -> InferM (Located Name))
    -> [Doc] -> [Pattern Name] -> [Prop] -> [InferM (Located Name)]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 Doc -> Pattern Name -> Prop -> InferM (Located Name)
    checkP [Doc]
    descs [Pattern Name]
    ps [Prop]
    tys)
         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 :: Prop
    thing = Prop
    t }) | (x :: Located Name
    x,t :: 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 -> Prop -> InferM Expr
    checkE Expr Name
    e Prop
    tRes)

         let args :: [(Name, Prop)]
    args = [ (Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x, Prop
    t) | (x :: Located Name
    x,t :: 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 (m :: * -> *) a. Monad m => a -> m a
    return (((Name, Prop) -> Expr -> Expr) -> Expr -> [(Name, Prop)] -> Expr
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\(x :: Name
    x,t :: Prop
    t) b :: 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 []   = TVarSource -> Kind -> InferM Prop
    newType TVarSource
    LenOfSeq Kind
    KNum
    smallest [t :: Prop
    t]  = Prop -> InferM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    t
    smallest ts :: [Prop]
    ts   = do Prop
    a <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    LenOfSeq Kind
    KNum
                       ConstraintSource -> [Prop] -> InferM ()
    newGoals ConstraintSource
    CtComprehension [ Prop
    a Prop -> Prop -> Prop
    =#= (Prop -> Prop -> Prop) -> [Prop] -> Prop
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Prop -> Prop -> Prop
    tMin [Prop]
    ts ]
                       Prop -> InferM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    a

    checkP :: Doc -> P.Pattern Name -> Type -> InferM (Located Name)
    checkP :: Doc -> Pattern Name -> Prop -> InferM (Located Name)
    checkP desc :: Doc
    desc p :: Pattern Name
    p tGoal :: Prop
    tGoal =
      do (x :: Name
    x, t :: Located Prop
    t) <- Doc -> Pattern Name -> InferM (Name, Located Prop)
    inferP Doc
    desc Pattern Name
    p
         [Prop]
    ps <- Prop -> Prop -> InferM [Prop]
    unify Prop
    tGoal (Located Prop -> Prop
    forall a. Located a -> a
    thing Located Prop
    t)
         let rng :: Range
    rng   = Range -> Maybe Range -> Range
    forall a. a -> Maybe a -> a
    fromMaybe Range
    emptyRange (Maybe Range -> Range) -> Maybe Range -> Range
    forall a b. (a -> b) -> a -> b
    $ Pattern Name -> Maybe Range
    forall t. HasLoc t => t -> Maybe Range
    getLoc Pattern Name
    p
         let mkErr :: Prop -> InferM ()
    mkErr = Error -> InferM ()
    recordError (Error -> InferM ()) -> (Prop -> Error) -> Prop -> InferM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> [Goal] -> Error
    UnsolvedGoals Bool
    False ([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 (Doc -> ConstraintSource
    CtPattern Doc
    desc) 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 (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 :: Doc -> P.Pattern Name -> InferM (Name, Located Type)
    inferP :: Doc -> Pattern Name -> InferM (Name, Located Prop)
    inferP desc :: Doc
    desc pat :: Pattern Name
    pat =
      case Pattern Name
    pat of

        P.PVar x0 :: 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) (TVarSource -> Kind -> InferM Prop
    newType (Name -> TVarSource
    DefinitionOf (Located Name -> Name
    forall a. Located a -> a
    thing Located Name
    x0)) Kind
    KType)
             (Name, Located Prop) -> InferM (Name, Located Prop)
    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 :: Prop
    thing = Prop
    a })

        P.PTyped p :: Pattern Name
    p t :: Type Name
    t ->
          do Prop
    tSig <- Type Name -> Kind -> InferM Prop
    checkTypeOfKind Type Name
    t Kind
    KType
             Located Name
    ln   <- Doc -> Pattern Name -> Prop -> InferM (Located Name)
    checkP Doc
    desc Pattern Name
    p Prop
    tSig
             (Name, Located Prop) -> InferM (Name, Located Prop)
    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 :: Prop
    thing = Prop
    tSig })

        _ -> String -> [String] -> InferM (Name, Located Prop)
    forall a. String -> [String] -> a
    tcPanic "inferP" [ "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 p :: Pattern Name
    p e :: Expr Name
    e) =
      do (x :: Name
    x,t :: Located Prop
    t) <- Doc -> Pattern Name -> InferM (Name, Located Prop)
    inferP (String -> Doc
    text "a value bound by a generator in a comprehension") Pattern Name
    p
         Prop
    n     <- TVarSource -> Kind -> InferM Prop
    newType TVarSource
    LenOfCompGen Kind
    KNum
         Expr
    e'    <- Expr Name -> Prop -> InferM Expr
    checkE Expr Name
    e (Prop -> Prop -> Prop
    tSeq Prop
    n (Located Prop -> Prop
    forall a. Located a -> a
    thing Located Prop
    t))
         (Match, Name, Located Prop, Prop)
    -> InferM (Match, Name, Located Prop, Prop)
    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 b :: 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 (TVarSource -> Kind -> InferM Prop
    newType (Name -> TVarSource
    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 (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 (1::Int))

      | Bool
    otherwise = String -> [String] -> InferM (Match, Name, Located Prop, Prop)
    forall a. String -> [String] -> a
    tcPanic "inferMatch"
                          [ "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 _ [] = String
    -> [String] -> InferM ([Match], Map Name (Located Prop), Prop)
    forall a. HasCallStack => String -> [String] -> a
    panic "inferCArm" [ "Empty comprehension arm" ]
    inferCArm _ [m :: Match Name
    m] =
      do (m1 :: Match
    m1, x :: Name
    x, t :: Located Prop
    t, n :: 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 (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 armNum :: Int
    armNum (m :: Match Name
    m : ms :: [Match Name]
    ms) =
      do (m1 :: Match
    m1, x :: Name
    x, t :: Located Prop
    t, n :: Prop
    n)  <- Match Name -> InferM (Match, Name, Located Prop, Prop)
    inferMatch Match Name
    m
         (ms' :: [Match]
    ms', ds :: Map Name (Located Prop)
    ds, n' :: 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 (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 (\_ old :: 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 generalzation.
    -- 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 isTopLevel :: Bool
    isTopLevel isRec :: Bool
    isRec binds :: [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 (sigs :: [Bind Name]
    sigs,noSigs :: [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 { bMono :: Bool
    P.bMono = Bool
    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 exprMap :: 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 (newEnv :: [(Name, VarType)]
    newEnv,todos :: [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 (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)
    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 (sigsAndMonos :: [InferM Decl]
    sigsAndMonos,noSigGen :: [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)
    sequence [InferM Decl]
    noSigGen
                                   InferM ()
    simplifyAllConstraints
                                   [Decl] -> InferM [Decl]
    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 (bs1 :: [Decl]
    bs1,cs :: [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)
    sequence [InferM Decl]
    sigsAndMonos)
                         ([Decl], [Decl]) -> InferM ([Decl], [Decl])
    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)
    sequence [InferM Decl]
    sigsAndMonos
                         (bs1 :: [Decl]
    bs1, cs :: [Goal]
    cs) <- InferM ([Decl], [Goal])
    prepGen
                         [Decl]
    genCs     <- [Decl] -> [Goal] -> InferM [Decl]
    generalize [Decl]
    bs1 [Goal]
    cs
                         ([Decl], [Decl]) -> InferM ([Decl], [Decl])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Decl]
    done,[Decl]
    genCs)

         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)
           (doneBs :: [Decl]
    doneBs, genBs :: [Decl]
    genBs) <- Map Name Expr -> InferM ([Decl], [Decl])
    check Map Name Expr
    exprMap

         InferM ()
    simplifyAllConstraints

         [Decl] -> InferM [Decl]
    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 d :: Decl
    d = (Decl -> Name
    dName Decl
    d, Schema -> VarType
    ExtVar (Decl -> Schema
    dSignature Decl
    d))
      isExt :: (a, VarType) -> Bool
    isExt (_,y :: VarType
    y) = case VarType
    y of
                      ExtVar _ -> Bool
    True
                      _        -> Bool
    False

      monoUse :: Decl -> (Name, Expr)
    monoUse d :: 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 e :: Expr
    e a :: TParam
    a = Expr -> Prop -> Expr
    ETApp Expr
    e (TVar -> Prop
    TVar (TParam -> TVar
    tpVar TParam
    a))
        appP :: Expr -> p -> Expr
    appP e :: Expr
    e _ = Expr -> Expr
    EProofApp Expr
    e

        withTys :: Expr
    withTys  = (Expr -> TParam -> Expr) -> Expr -> [TParam] -> Expr
    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 (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

    {- | 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 exprMap :: Map Name Expr
    exprMap b :: Bind Name
    b@(P.Bind { .. }) =
      case Maybe (Schema Name)
    bSignature of

        Just s :: Schema Name
    s ->
          do (Schema, [Goal])
    s1 <- AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
    checkSchema AllowWildCards
    AllowWildCards Schema Name
    s
             ((Name, VarType), Either (InferM Decl) (InferM Decl))
    -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
    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))

        Nothing
          | Bool
    bMono ->
             do Prop
    t <- TVarSource -> Kind -> InferM Prop
    newType (Name -> TVarSource
    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 (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 <- TVarSource -> Kind -> InferM Prop
    newType (Name -> TVarSource
    DefinitionOf Name
    name) Kind
    KType
               let noWay :: a
    noWay = String -> [String] -> a
    forall a. String -> [String] -> a
    tcPanic "guessType" [ "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 (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 [] gs0 :: [Goal]
    gs0 =
      do [Goal] -> InferM ()
    addGoals [Goal]
    gs0
         [Decl] -> InferM [Decl]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    generalize bs0 :: [Decl]
    bs0 gs0 :: [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
    $ \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 (m :: * -> *) a. Monad m => a -> m a
    return Decl
    b { dSignature :: Schema
    dSignature = Schema
    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 g :: 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 g :: 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
             (here0 :: [Goal]
    here0,later :: [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 (as0 :: [TVar]
    as0,here1 :: [Goal]
    here1,defSu :: Subst
    defSu,ws :: [Warning]
    ws) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    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
         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 = [ $WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
    TParam { tpUnique :: Int
    tpUnique = Int
    x, tpKind :: Kind
    tpKind = Kind
    k, tpFlav :: TPFlavor
    tpFlav = Maybe Name -> TPFlavor
    TPOther Maybe Name
    forall a. Maybe a
    Nothing
                             , tpInfo :: TVarInfo
    tpInfo = TVarInfo
    i  } | TVFree x :: Int
    x k :: Kind
    k _ i :: 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 e :: Expr
    e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    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 (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 d :: Decl
    d = Decl
    d { dDefinition :: DeclDef
    dDefinition = case Decl -> DeclDef
    dDefinition Decl
    d of
                                          DExpr e :: Expr
    e -> Expr -> DeclDef
    DExpr (Expr -> Expr
    genE Expr
    e)
                                          DPrim   -> DeclDef
    DPrim
                        , dSignature :: Schema
    dSignature  = [TParam] -> [Prop] -> Prop -> Schema
    Forall [TParam]
    asPs [Prop]
    qs
                                      (Prop -> Schema) -> Prop -> Schema
    forall a b. (a -> b) -> a -> b
    $ Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Prop -> Prop) -> Prop -> Prop
    forall a b. (a -> b) -> a -> b
    $ Schema -> Prop
    sType (Schema -> Prop) -> Schema -> Prop
    forall a b. (a -> b) -> a -> b
    $ Decl -> Schema
    dSignature Decl
    d
                        }

         [Decl] -> InferM [Decl]
    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 x :: t
    x y :: 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
                     (KNum, KNum) -> Ordering
    EQ
                     (KNum, _)    -> Ordering
    LT
                     (_,KNum)     -> Ordering
    GT
                     _            -> Ordering
    EQ

    -- | Check a monomorphic binding.
    checkMonoB :: P.Bind Name -> Type -> InferM Decl
    checkMonoB :: Bind Name -> Prop -> InferM Decl
    checkMonoB b :: Bind Name
    b t :: 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

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

        P.DExpr e :: Expr Name
    e ->
          do Expr
    e1 <- Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
    checkFun (Name -> Doc
    forall a. PP a => a -> Doc
    pp (Located Name -> Name
    forall a. Located a -> a
    thing (Bind Name -> Located Name
    forall name. Bind name -> Located name
    P.bName Bind Name
    b))) (Bind Name -> [Pattern Name]
    forall name. Bind name -> [Pattern name]
    P.bParams Bind Name
    b) Expr Name
    e Prop
    t
             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 (m :: * -> *) a. Monad m => a -> m a
    return $WDecl :: Name
    -> Schema
    -> DeclDef
    -> [Pragma]
    -> Bool
    -> Maybe Fixity
    -> Maybe String
    -> Decl
    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 String
    dDoc = Bind Name -> Maybe String
    forall name. Bind name -> Maybe String
    P.bDoc 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 b :: Bind Name
    b (Forall as :: [TParam]
    as asmps0 :: [Prop]
    asmps0 t0 :: Prop
    t0, validSchema :: [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?
     P.DPrim ->
       do Decl -> InferM Decl
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WDecl :: Name
    -> Schema
    -> DeclDef
    -> [Pragma]
    -> Bool
    -> Maybe Fixity
    -> Maybe String
    -> Decl
    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]
    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 String
    dDoc        = Bind Name -> Maybe String
    forall name. Bind name -> Maybe String
    P.bDoc Bind Name
    b
                      }

     P.DExpr e0 :: Expr Name
    e0 ->
      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
    $
      [TParam] -> InferM Decl -> InferM Decl
    forall a. [TParam] -> InferM a -> InferM a
    withTParams [TParam]
    as (InferM Decl -> InferM Decl) -> InferM Decl -> InferM Decl
    forall a b. (a -> b) -> a -> b
    $
      do (e1 :: Expr
    e1,cs0 :: [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 Expr
    e1 <- Doc -> [Pattern Name] -> Expr Name -> Prop -> InferM Expr
    checkFun (Name -> Doc
    forall a. PP a => a -> Doc
    pp (Located Name -> Name
    forall a. Located a -> a
    thing (Bind Name -> Located Name
    forall name. Bind name -> Located name
    P.bName Bind Name
    b))) (Bind Name -> [Pattern Name]
    forall name. Bind name -> [Pattern name]
    P.bParams Bind Name
    b) Expr Name
    e0 Prop
    t0
                       [Goal] -> InferM ()
    addGoals [Goal]
    validSchema
                       () <- InferM ()
    simplifyAllConstraints  -- XXX: using `asmps` also?
                       Expr -> InferM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e1
         [Goal]
    cs <- [Goal] -> InferM [Goal]
    applySubstGoals [Goal]
    cs0

         let findKeep :: Set a -> [a] -> [(a, Set a)] -> ([a], [a])
    findKeep vs :: Set a
    vs keep :: [a]
    keep todo :: [(a, Set a)]
    todo =
              let stays :: (a, Set a) -> Bool
    stays (_,cvs :: 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
                  (yes :: [(a, Set a)]
    yes,perhaps :: [(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
                  (stayPs :: [a]
    stayPs,newVars :: [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)
                   _  -> 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 (stay :: [Goal]
    stay,leave :: [Goal]
    leave) = Set TVar -> [Goal] -> [(Goal, Set TVar)] -> ([Goal], [Goal])
    forall a a. Ord a => Set a -> [a] -> [(a, Set a)] -> ([a], [a])
    findKeep ([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)) []
                                [ (Goal
    c, Goal -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Goal
    c) | Goal
    c <- [Goal]
    cs ]

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

         [Prop]
    asmps1 <- [Prop] -> InferM [Prop]
    applySubstPreds [Prop]
    asmps0

         Subst
    su <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication (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]
    asmps1 [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]
    asmps1)
         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

         Decl -> InferM Decl
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WDecl :: Name
    -> Schema
    -> DeclDef
    -> [Pragma]
    -> Bool
    -> Maybe Fixity
    -> Maybe String
    -> Decl
    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 = Expr -> DeclDef
    DExpr ((TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    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 (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Expr -> Expr
    EProofAbs Expr
    e2 [Prop]
    asmps) [TParam]
    as)
            , 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 String
    dDoc        = Bind Name -> Maybe String
    forall name. Bind name -> Maybe String
    P.bDoc Bind Name
    b
            }

    inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
    inferDs :: [d] -> ([DeclGroup] -> InferM a) -> InferM a
    inferDs ds :: [d]
    ds continue :: [DeclGroup] -> InferM a
    continue = [TyDecl] -> InferM a
    checkTyDecls ([TyDecl] -> InferM a) -> InferM [TyDecl] -> InferM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TyDecl] -> InferM [TyDecl]
    orderTyDecls ((d -> Maybe TyDecl) -> [d] -> [TyDecl]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe d -> Maybe TyDecl
    forall d. FromDecl d => d -> Maybe TyDecl
    toTyDecl [d]
    ds)
      where
      isTopLevel :: Bool
    isTopLevel = d -> Bool
    forall d. FromDecl d => d -> Bool
    isTopDecl ([d] -> d
    forall a. [a] -> a
    head [d]
    ds)

      checkTyDecls :: [TyDecl] -> InferM a
    checkTyDecls (AT t :: ParameterType Name
    t mbD :: Maybe String
    mbD : ts :: [TyDecl]
    ts) =
        do ModTParam
    t1 <- ParameterType Name -> Maybe String -> InferM ModTParam
    checkParameterType ParameterType Name
    t Maybe String
    mbD
           ModTParam -> InferM a -> InferM a
    forall a. ModTParam -> InferM a -> InferM a
    withParamType ModTParam
    t1 ([TyDecl] -> InferM a
    checkTyDecls [TyDecl]
    ts)

      checkTyDecls (TS t :: TySyn Name
    t mbD :: Maybe String
    mbD : ts :: [TyDecl]
    ts) =
        do TySyn
    t1 <- TySyn Name -> Maybe String -> InferM TySyn
    checkTySyn TySyn Name
    t Maybe String
    mbD
           TySyn -> InferM a -> InferM a
    forall a. TySyn -> InferM a -> InferM a
    withTySyn TySyn
    t1 ([TyDecl] -> InferM a
    checkTyDecls [TyDecl]
    ts)

      checkTyDecls (PS t :: PropSyn Name
    t mbD :: Maybe String
    mbD : ts :: [TyDecl]
    ts) =
        do TySyn
    t1 <- PropSyn Name -> Maybe String -> InferM TySyn
    checkPropSyn PropSyn Name
    t Maybe String
    mbD
           TySyn -> InferM a -> InferM a
    forall a. TySyn -> InferM a -> InferM a
    withTySyn TySyn
    t1 ([TyDecl] -> InferM a
    checkTyDecls [TyDecl]
    ts)

      checkTyDecls (NT t :: Newtype Name
    t mbD :: Maybe String
    mbD : ts :: [TyDecl]
    ts) =
        do Newtype
    t1 <- Newtype Name -> Maybe String -> InferM Newtype
    checkNewtype Newtype Name
    t Maybe String
    mbD
           Newtype -> InferM a -> InferM a
    forall a. Newtype -> InferM a -> InferM a
    withNewtype Newtype
    t1 ([TyDecl] -> InferM a
    checkTyDecls [TyDecl]
    ts)

      checkTyDecls (PT p :: PrimType Name
    p mbD :: Maybe String
    mbD : ts :: [TyDecl]
    ts) =
        do AbstractType
    p1 <- PrimType Name -> Maybe String -> InferM AbstractType
    checkPrimType PrimType Name
    p Maybe String
    mbD
           AbstractType -> InferM a -> InferM a
    forall a. AbstractType -> InferM a -> InferM a
    withPrimType AbstractType
    p1 ([TyDecl] -> InferM a
    checkTyDecls [TyDecl]
    ts)

      -- We checked all type synonyms, now continue with value-level definitions:
      checkTyDecls [] =
        do [Located Prop]
    cs <- [Located (Prop Name)] -> InferM [Located Prop]
    checkParameterConstraints ((d -> [Located (Prop Name)]) -> [d] -> [Located (Prop Name)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap d -> [Located (Prop Name)]
    forall d. FromDecl d => d -> [Located (Prop Name)]
    toParamConstraints [d]
    ds)
           [Located Prop] -> InferM a -> InferM a
    forall a. [Located Prop] -> InferM a -> InferM a
    withParameterConstraints [Located Prop]
    cs (InferM a -> InferM a) -> InferM a -> InferM a
    forall a b. (a -> b) -> a -> b
    $
             do [ModVParam]
    xs <- (ParameterFun Name -> InferM ModVParam)
    -> [ParameterFun Name] -> InferM [ModVParam]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ParameterFun Name -> InferM ModVParam
    checkParameterFun ((d -> Maybe (ParameterFun Name)) -> [d] -> [ParameterFun Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe d -> Maybe (ParameterFun Name)
    forall d. FromDecl d => d -> Maybe (ParameterFun Name)
    toParamFun [d]
    ds)
                [ModVParam] -> InferM a -> InferM a
    forall a. [ModVParam] -> InferM a -> InferM a
    withParamFuns [ModVParam]
    xs (InferM a -> InferM a) -> InferM a -> InferM a
    forall a b. (a -> b) -> a -> b
    $ [DeclGroup] -> [SCC (Bind Name)] -> InferM a
    checkBinds [] ([SCC (Bind Name)] -> InferM a) -> [SCC (Bind Name)] -> InferM a
    forall a b. (a -> b) -> a -> b
    $ [Bind Name] -> [SCC (Bind Name)]
    orderBinds ([Bind Name] -> [SCC (Bind Name)])
    -> [Bind Name] -> [SCC (Bind Name)]
    forall a b. (a -> b) -> a -> b
    $ (d -> Maybe (Bind Name)) -> [d] -> [Bind Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe d -> Maybe (Bind Name)
    forall d. FromDecl d => d -> Maybe (Bind Name)
    toBind [d]
    ds

      checkParameterFun :: ParameterFun Name -> InferM ModVParam
    checkParameterFun x :: ParameterFun Name
    x =
        do (s :: Schema
    s,gs :: [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 <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication (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 "checkParameterFun" ["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 (m :: * -> *) a. Monad m => a -> m a
    return ModVParam :: Name -> Schema -> Maybe String -> Maybe Fixity -> ModVParam
    ModVParam { mvpName :: Name
    mvpName = Name
    n
                            , mvpType :: Schema
    mvpType = Schema
    s
                            , mvpDoc :: Maybe String
    mvpDoc  = ParameterFun Name -> Maybe String
    forall name. ParameterFun name -> Maybe String
    P.pfDoc ParameterFun Name
    x
                            , mvpFixity :: Maybe Fixity
    mvpFixity = ParameterFun Name -> Maybe Fixity
    forall name. ParameterFun name -> Maybe Fixity
    P.pfFixity ParameterFun Name
    x
                            }

      checkBinds :: [DeclGroup] -> [SCC (Bind Name)] -> InferM a
    checkBinds decls :: [DeclGroup]
    decls (CyclicSCC bs :: [Bind Name]
    bs : more :: [SCC (Bind Name)]
    more) =
         do [Decl]
    bs1 <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
    inferBinds Bool
    isTopLevel Bool
    True [Bind Name]
    bs
            (Decl -> InferM a -> InferM a) -> InferM a -> [Decl] -> InferM a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\b :: Decl
    b m :: InferM a
    m -> Name -> Schema -> InferM a -> InferM a
    forall a. Name -> Schema -> InferM a -> InferM a
    withVar (Decl -> Name
    dName Decl
    b) (Decl -> Schema
    dSignature Decl
    b) InferM a
    m)
                  ([DeclGroup] -> [SCC (Bind Name)] -> InferM a
    checkBinds ([Decl] -> DeclGroup
    Recursive [Decl]
    bs1 DeclGroup -> [DeclGroup] -> [DeclGroup]
    forall a. a -> [a] -> [a]
    : [DeclGroup]
    decls) [SCC (Bind Name)]
    more)
                  [Decl]
    bs1

      checkBinds decls :: [DeclGroup]
    decls (AcyclicSCC c :: Bind Name
    c : more :: [SCC (Bind Name)]
    more) =
        do ~[b :: Decl
    b] <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
    inferBinds Bool
    isTopLevel Bool
    False [Bind Name
    c]
           Name -> Schema -> InferM a -> InferM a
    forall a. Name -> Schema -> InferM a -> InferM a
    withVar (Decl -> Name
    dName Decl
    b) (Decl -> Schema
    dSignature Decl
    b) (InferM a -> InferM a) -> InferM a -> InferM a
    forall a b. (a -> b) -> a -> b
    $
             [DeclGroup] -> [SCC (Bind Name)] -> InferM a
    checkBinds (Decl -> DeclGroup
    NonRecursive Decl
    b DeclGroup -> [DeclGroup] -> [DeclGroup]
    forall a. a -> [a] -> [a]
    : [DeclGroup]
    decls) [SCC (Bind Name)]
    more

      -- We are done with all value-level definitions.
      -- Now continue with anything that's in scope of the declarations.
      checkBinds decls :: [DeclGroup]
    decls [] = [DeclGroup] -> InferM a
    continue ([DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a]
    reverse [DeclGroup]
    decls)

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