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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        P.EGenerate   {} -> InferM Expr
    mono

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    -}

    inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
    inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
    inferBinds Bool
    isTopLevel Bool
    isRec [Bind Name]
    binds =
      do -- when mono-binds is enabled, and we're not checking top-level
         -- declarations, mark all bindings lacking signatures as monomorphic
         Bool
    monoBinds <- InferM Bool
    getMonoBinds
         let ([Bind Name]
    sigs,[Bind Name]
    noSigs) = (Bind Name -> Bool) -> [Bind Name] -> ([Bind Name], [Bind Name])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (Maybe (Schema Name) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (Schema Name) -> Bool)
    -> (Bind Name -> Maybe (Schema Name)) -> Bind Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bind Name -> Maybe (Schema Name)
    forall name. Bind name -> Maybe (Schema name)
    P.bSignature) [Bind Name]
    binds
             monos :: [Bind Name]
    monos         = [Bind Name]
    sigs [Bind Name] -> [Bind Name] -> [Bind Name]
    forall a. [a] -> [a] -> [a]
    ++ [ Bind Name
    b { 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 Map Name Expr
    exprMap =
            {- Guess type is here, because while we check user supplied signatures
               we may generate additional constraints. For example, `x - y` would
               generate an additional constraint `x >= y`. -}
               do ([(Name, VarType)]
    newEnv,[Either (InferM Decl) (InferM Decl)]
    todos) <- [((Name, VarType), Either (InferM Decl) (InferM Decl))]
    -> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([((Name, VarType), Either (InferM Decl) (InferM Decl))]
     -> ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)]))
    -> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
    -> InferM ([(Name, VarType)], [Either (InferM Decl) (InferM Decl)])
    forall a b. (a -> b) -> InferM a -> InferM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (Bind Name
     -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl)))
    -> [Bind Name]
    -> InferM [((Name, VarType), Either (InferM Decl) (InferM Decl))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Map Name Expr
    -> Bind Name
    -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
    guessType Map Name Expr
    exprMap) [Bind Name]
    binds'
                  let otherEnv :: [(Name, VarType)]
    otherEnv = ((Name, VarType) -> Bool) -> [(Name, VarType)] -> [(Name, VarType)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name, VarType) -> Bool
    forall {a}. (a, VarType) -> Bool
    isExt [(Name, VarType)]
    newEnv

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

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

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

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

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

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

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

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

         InferM ()
    simplifyAllConstraints

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

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

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

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

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

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

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

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

      hasConstraintGuards :: Bind name -> Bool
    hasConstraintGuards Bind name
    b =
        case 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.DPropGuards {} -> Bool
    True
          BindDef name
    _                -> Bool
    False

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

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

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

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

          | Bool
    otherwise ->

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

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

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

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

    generalize [Decl]
    bs0 [Goal]
    gs0 =
      do {- First, we apply the accumulating substitution to the goals
            and the inferred types, to ensure that we have the most up
            to date information. -}
         [Goal]
    gs <- [Goal] -> InferM [Goal]
    applySubstGoals [Goal]
    gs0
         [Decl]
    bs <- [Decl] -> (Decl -> InferM Decl) -> InferM [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Decl]
    bs0 ((Decl -> InferM Decl) -> InferM [Decl])
    -> (Decl -> InferM Decl) -> InferM [Decl]
    forall a b. (a -> b) -> a -> b
    $ \Decl
    b -> do Schema
    s <- Schema -> InferM Schema
    forall t. TVars t => t -> InferM t
    applySubst (Decl -> Schema
    dSignature Decl
    b)
                                   Decl -> InferM Decl
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Decl
    b { dSignature :: 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 Goal
    g  = (TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Prop -> Set TVar) -> Prop -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ Goal -> Prop
    goal Goal
    g
             inGoals :: Set TVar
    inGoals    = [Set TVar] -> Set TVar
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ (Goal -> Set TVar) -> [Goal] -> [Set TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Set TVar
    goalFVS [Goal]
    gs
             inSigs :: Set TVar
    inSigs     = (TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV (Set TVar -> Set TVar) -> Set TVar -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ [Schema] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs ([Schema] -> Set TVar) -> [Schema] -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ (Decl -> Schema) -> [Decl] -> [Schema]
    forall a b. (a -> b) -> [a] -> [b]
    map Decl -> Schema
    dSignature [Decl]
    bs
             candidates :: Set TVar
    candidates = (Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set TVar
    inGoals Set TVar
    inSigs)

         Set TVar
    asmpVs <- InferM (Set TVar)
    varsWithAsmps

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

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

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

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

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

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

             genE :: Expr -> Expr
    genE Expr
    e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Expr -> Expr
    ETAbs ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Expr -> Expr
    EProofAbs (Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e) [Prop]
    qs) [TParam]
    asPs
             genB :: Decl -> Decl
    genB Decl
    d = Decl
    d { dDefinition :: DeclDef
    dDefinition = case Decl -> DeclDef
    dDefinition Decl
    d of
                                          DExpr Expr
    e    -> Expr -> DeclDef
    DExpr (Expr -> Expr
    genE Expr
    e)
                                          DeclDef
    DPrim      -> DeclDef
    DPrim
                                          DForeign FFIFunType
    t -> FFIFunType -> DeclDef
    DForeign FFIFunType
    t
                        , 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 a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Decl -> Decl) -> [Decl] -> [Decl]
    forall a b. (a -> b) -> [a] -> [b]
    map Decl -> Decl
    genB [Decl]
    bs)

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

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

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

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

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

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

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

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

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

        P.DExpr 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
            (Prop
    t, [Prop]
    asmps, Expr
    e2) <- [Prop] -> [Prop] -> Expr Name -> InferM (Prop, [Prop], Expr)
    checkBindDefExpr [] [Prop]
    asmps0 Expr Name
    e0

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

        P.DPropGuards [PropGuardCase Name]
    cases0 ->
          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
              [Prop]
    asmps1 <- [Prop] -> InferM [Prop]
    applySubstPreds [Prop]
    asmps0
              Prop
    t1     <- Prop -> InferM Prop
    forall t. TVars t => t -> InferM t
    applySubst Prop
    t0
              [([Prop], Expr)]
    cases1 <- (PropGuardCase Name -> InferM ([Prop], Expr))
    -> [PropGuardCase Name] -> InferM [([Prop], Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM PropGuardCase Name -> InferM ([Prop], Expr)
    checkPropGuardCase [PropGuardCase Name]
    cases0

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

              let schema :: Schema
    schema = [TParam] -> [Prop] -> Prop -> Schema
    Forall [TParam]
    as [Prop]
    asmps1 Prop
    t1

              Decl -> InferM Decl
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Decl
                { dName :: Name
    dName       = Name
    name
                , dSignature :: Schema
    dSignature  = Schema
    schema
                , dDefinition :: DeclDef
    dDefinition = Expr -> DeclDef
    DExpr
                                  ((TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Expr -> Expr
    ETAbs
                                    ((Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Expr -> Expr
    EProofAbs
                                      ([([Prop], Expr)] -> Prop -> Expr
    EPropGuards [([Prop], Expr)]
    cases1 Prop
    t1)
                                    [Prop]
    asmps1)
                                  [TParam]
    as)
                , dPragmas :: [Pragma]
    dPragmas    = Bind Name -> [Pragma]
    forall name. Bind name -> [Pragma]
    P.bPragmas Bind Name
    b
                , dInfix :: Bool
    dInfix      = Bind Name -> Bool
    forall name. Bind name -> Bool
    P.bInfix Bind Name
    b
                , dFixity :: Maybe Fixity
    dFixity     = Bind Name -> Maybe Fixity
    forall name. Bind name -> Maybe Fixity
    P.bFixity Bind Name
    b
                , dDoc :: Maybe Text
    dDoc        = Bind Name -> Maybe Text
    forall name. Bind name -> Maybe Text
    P.bDoc Bind Name
    b
                }

      where

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

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

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

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

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

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

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

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

    {- |
    Given a DPropGuards of the form

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

         InferM ()
    proveModuleTopLevel

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

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

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

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

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

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

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

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

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

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

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

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

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