    -- |
    -- Module      :  Cryptol.TypeCheck.Sanity
    -- Copyright   :  (c) 2015-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    {-# Language OverloadedStrings #-}
    module Cryptol.TypeCheck.Sanity
      ( tcExpr
      , tcDecls
      , tcModule
      , ProofObligation
      , onlyNonTrivial
      , Error(..)
      , AreSame(..)
      , same
      ) where

    import Cryptol.Parser.Position(thing,Range,emptyRange)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
    import Cryptol.TypeCheck.Monad(InferInput(..))
    import Cryptol.ModuleSystem.Name(nameLoc)
    import Cryptol.Utils.Ident
    import Cryptol.Utils.RecordMap
    import Cryptol.Utils.PP

    import Data.List (sort)
    import qualified Data.Set as Set
    import MonadLib
    import qualified Control.Applicative as A

    import           Data.Map ( Map )
    import qualified Data.Map as Map

    tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [ ProofObligation ])
    tcExpr :: InferInput -> Expr -> Either (Range, Error) (Schema, [Schema])
    tcExpr InferInput
    env Expr
    e = InferInput
    -> TcM Schema -> Either (Range, Error) (Schema, [Schema])
    forall a.
    InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
    runTcM InferInput
    env (Expr -> TcM Schema
    exprSchema Expr
    e)

    tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [ ProofObligation ]
    tcDecls :: InferInput -> [DeclGroup] -> Either (Range, Error) [Schema]
    tcDecls InferInput
    env [DeclGroup]
    ds0 = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
    forall a.
    InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
    runTcM InferInput
    env ([DeclGroup] -> TcM ()
    checkDecls [DeclGroup]
    ds0) of
                        Left (Range, Error)
    err     -> (Range, Error) -> Either (Range, Error) [Schema]
    forall a b. a -> Either a b
    Left (Range, Error)
    err
                        Right (()
    _,[Schema]
    ps) -> [Schema] -> Either (Range, Error) [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    ps

    tcModule :: InferInput -> Module -> Either (Range, Error) [ ProofObligation ]
    tcModule :: InferInput -> Module -> Either (Range, Error) [Schema]
    tcModule InferInput
    env Module
    m = case InferInput -> TcM () -> Either (Range, Error) ((), [Schema])
    forall a.
    InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
    runTcM InferInput
    env TcM ()
    check of
                       Left (Range, Error)
    err -> (Range, Error) -> Either (Range, Error) [Schema]
    forall a b. a -> Either a b
    Left (Range, Error)
    err
                       Right (()
    _,[Schema]
    ps) -> [Schema] -> Either (Range, Error) [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    ps
      where check :: TcM ()
    check = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> TcM () -> TcM ()
    forall a. TParam -> TcM a -> TcM a
    withTVar TcM ()
    k1 ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam (Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems (Module -> Map Name ModTParam
    forall mname. ModuleG mname -> Map Name ModTParam
    mParamTypes Module
    m)))
            k1 :: TcM ()
    k1    = (Type -> TcM () -> TcM ()) -> TcM () -> [Type] -> TcM ()
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Type -> TcM () -> TcM ()
    forall a. Type -> TcM a -> TcM a
    withAsmp TcM ()
    k2 ((Located Type -> Type) -> [Located Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Type -> Type
    forall a. Located a -> a
    thing (Module -> [Located Type]
    forall mname. ModuleG mname -> [Located Type]
    mParamConstraints Module
    m))
            k2 :: TcM ()
    k2    = [(Name, Schema)] -> TcM () -> TcM ()
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars (Map Name Schema -> [(Name, Schema)]
    forall k a. Map k a -> [(k, a)]
    Map.toList ((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
    forall a b. (a -> b) -> Map Name a -> Map Name b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModVParam -> Schema
    mvpType (Module -> Map Name ModVParam
    forall mname. ModuleG mname -> Map Name ModVParam
    mParamFuns Module
    m)))
                  (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ [DeclGroup] -> TcM ()
    checkDecls (Module -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls Module
    m)

    onlyNonTrivial :: [ProofObligation] -> [ProofObligation]
    onlyNonTrivial :: [Schema] -> [Schema]
    onlyNonTrivial = (Schema -> Bool) -> [Schema] -> [Schema]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Schema -> Bool) -> Schema -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Schema -> Bool
    trivialProofObligation)

    -- | Identify proof obligations that are obviously true.
    -- We can filter these to avoid clutter
    trivialProofObligation :: ProofObligation -> Bool
    trivialProofObligation :: Schema -> Bool
    trivialProofObligation Schema
    oblig = Type -> Bool
    pIsTrue Type
    goal Bool -> Bool -> Bool
    || Bool
    simpleEq Bool -> Bool -> Bool
    || Type
    goal Type -> [Type] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Type]
    asmps
      where
      goal :: Type
    goal  = Schema -> Type
    sType Schema
    oblig
      asmps :: [Type]
    asmps = Schema -> [Type]
    sProps Schema
    oblig
      simpleEq :: Bool
    simpleEq = case Type -> Maybe (Type, Type)
    pIsEqual Type
    goal of
                   Just (Type
    t1,Type
    t2) -> Type
    t1 Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    t2
                   Maybe (Type, Type)
    Nothing      -> Bool
    False

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

    checkDecls :: [DeclGroup] -> TcM ()
    checkDecls :: [DeclGroup] -> TcM ()
    checkDecls [DeclGroup]
    decls =
      case [DeclGroup]
    decls of
        [] -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        DeclGroup
    d : [DeclGroup]
    ds -> do [(Name, Schema)]
    xs <- DeclGroup -> TcM [(Name, Schema)]
    checkDeclGroup DeclGroup
    d
                     [(Name, Schema)] -> TcM () -> TcM ()
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)]
    xs ([DeclGroup] -> TcM ()
    checkDecls [DeclGroup]
    ds)

    -- | Validate a type, returning its kind.
    checkType :: Type -> TcM Kind
    checkType :: Type -> TcM Kind
    checkType Type
    ty =
      case Type
    ty of
        TUser Name
    _ [Type]
    _ Type
    t -> Type -> TcM Kind
    checkType Type
    t    -- Maybe check synonym too?

        TCon TCon
    tc [Type]
    ts ->
          do [Kind]
    ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
    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 -> TcM Kind
    checkType [Type]
    ts
             Kind -> [Kind] -> TcM Kind
    checkKind (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc) [Kind]
    ks

        TNewtype Newtype
    nt [Type]
    ts ->
          do [Kind]
    ks <- (Type -> TcM Kind) -> [Type] -> TcM [Kind]
    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 -> TcM Kind
    checkType [Type]
    ts
             Kind -> [Kind] -> TcM Kind
    checkKind (Newtype -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Newtype
    nt) [Kind]
    ks

        TVar TVar
    tv -> TVar -> TcM Kind
    lookupTVar TVar
    tv

        TRec RecordMap Ident Type
    fs ->
          do RecordMap Ident Type -> (Type -> TcM ()) -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ RecordMap Ident Type
    fs ((Type -> TcM ()) -> TcM ()) -> (Type -> TcM ()) -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ \Type
    t ->
               do Kind
    k <- Type -> TcM Kind
    checkType Type
    t
                  Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KType) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch Kind
    KType Kind
    k
             Kind -> TcM Kind
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KType

      where
      checkKind :: Kind -> [Kind] -> TcM Kind
    checkKind Kind
    k [] = case Kind
    k of
                         Kind
    _ :-> Kind
    _  -> Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (Error -> TcM Kind) -> Error -> TcM Kind
    forall a b. (a -> b) -> a -> b
    $ Kind -> Error
    NotEnoughArgumentsInKind Kind
    k
                         Kind
    KProp    -> Kind -> TcM Kind
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
                         Kind
    KNum     -> Kind -> TcM Kind
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
                         Kind
    KType    -> Kind -> TcM Kind
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k

      checkKind (Kind
    k1 :-> Kind
    k2) (Kind
    k : [Kind]
    ks)
        | Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k1   = Kind -> [Kind] -> TcM Kind
    checkKind Kind
    k2 [Kind]
    ks
        | Bool
    otherwise = Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (Error -> TcM Kind) -> Error -> TcM Kind
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch Kind
    k1 Kind
    k

      checkKind Kind
    k [Kind]
    ks = Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (Error -> TcM Kind) -> Error -> TcM Kind
    forall a b. (a -> b) -> a -> b
    $ Kind -> [Kind] -> Error
    BadTypeApplication Kind
    k [Kind]
    ks

    -- | Check that the type is valid, and it has the given kind.
    checkTypeIs :: Kind -> Type -> TcM ()
    checkTypeIs :: Kind -> Type -> TcM ()
    checkTypeIs Kind
    k Type
    ty =
      do Kind
    k1 <- Type -> TcM Kind
    checkType Type
    ty
         Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k1) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch Kind
    k Kind
    k1

    -- | Check that this is a valid schema.
    checkSchema :: Schema -> TcM ()
    checkSchema :: Schema -> TcM ()
    checkSchema (Forall [TParam]
    as [Type]
    ps Type
    t) = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> TcM () -> TcM ()
    forall a. TParam -> TcM a -> TcM a
    withTVar TcM ()
    check [TParam]
    as
      where check :: TcM ()
    check = do (Type -> TcM ()) -> [Type] -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Kind -> Type -> TcM ()
    checkTypeIs Kind
    KProp) [Type]
    ps
                       Kind -> Type -> TcM ()
    checkTypeIs Kind
    KType Type
    t

    data AreSame = SameIf [Prop]
                 | NotSame

    areSame :: AreSame
    areSame :: AreSame
    areSame = [Type] -> AreSame
    SameIf []

    sameAnd :: AreSame -> AreSame -> AreSame
    sameAnd :: AreSame -> AreSame -> AreSame
    sameAnd AreSame
    x AreSame
    y =
      case (AreSame
    x,AreSame
    y) of
        (SameIf [Type]
    xs, SameIf [Type]
    ys) -> [Type] -> AreSame
    SameIf ([Type]
    xs [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ [Type]
    ys)
        (AreSame, AreSame)
    _                      -> AreSame
    NotSame

    sameBool :: Bool -> AreSame
    sameBool :: Bool -> AreSame
    sameBool Bool
    b = if Bool
    b then AreSame
    areSame else AreSame
    NotSame

    sameTypes :: String -> Type -> Type -> TcM ()
    sameTypes :: String -> Type -> Type -> TcM ()
    sameTypes String
    msg Type
    x Type
    y = String -> Schema -> Schema -> TcM ()
    sameSchemas String
    msg (Type -> Schema
    tMono Type
    x) (Type -> Schema
    tMono Type
    y)

    sameSchemas :: String -> Schema -> Schema -> TcM ()
    sameSchemas :: String -> Schema -> Schema -> TcM ()
    sameSchemas String
    msg Schema
    x Schema
    y =
      case Schema -> Schema -> AreSame
    forall a. Same a => a -> a -> AreSame
    same Schema
    x Schema
    y of
        AreSame
    NotSame   -> Error -> TcM ()
    forall a. Error -> TcM a
    reportError (String -> Schema -> Schema -> Error
    TypeMismatch String
    msg Schema
    x Schema
    y)
        SameIf [Type]
    ps -> (Type -> TcM ()) -> [Type] -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Type -> TcM ()
    proofObligation [Type]
    ps

    class Same a where
      same :: a -> a -> AreSame

    instance Same a => Same [a] where
      same :: [a] -> [a] -> AreSame
    same [] [] = AreSame
    areSame
      same (a
    x : [a]
    xs) (a
    y : [a]
    ys) = a -> a -> AreSame
    forall a. Same a => a -> a -> AreSame
    same a
    x a
    y AreSame -> AreSame -> AreSame
    `sameAnd` [a] -> [a] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same [a]
    xs [a]
    ys
      same [a]
    _ [a]
    _ = AreSame
    NotSame

    data Field a b = Field a b

    instance (Eq a, Same b) => Same (Field a b) where
      same :: Field a b -> Field a b -> AreSame
    same (Field a
    x b
    a) (Field a
    y b
    b) = Bool -> AreSame
    sameBool (a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y) AreSame -> AreSame -> AreSame
    `sameAnd` b -> b -> AreSame
    forall a. Same a => a -> a -> AreSame
    same b
    a b
    b

    instance Same Type where
      same :: Type -> Type -> AreSame
    same Type
    t1 Type
    t2
        | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    k2    = AreSame
    NotSame
        | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KNum  = if Type
    t1 Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type
    t2 then [Type] -> AreSame
    SameIf [] else [Type] -> AreSame
    SameIf [ Type
    t1 Type -> Type -> Type
    =#= Type
    t2 ]
        | Bool
    otherwise   =
          case (Type -> Type
    tNoUser Type
    t1, Type -> Type
    tNoUser Type
    t2) of
            (TVar TVar
    x, TVar TVar
    y)               -> Bool -> AreSame
    sameBool (TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y)
            (TRec RecordMap Ident Type
    x, TRec RecordMap Ident Type
    y)               -> [Field Ident Type] -> [Field Ident Type] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same (RecordMap Ident Type -> [Field Ident Type]
    forall {a} {b}. RecordMap a b -> [Field a b]
    mkRec RecordMap Ident Type
    x) (RecordMap Ident Type -> [Field Ident Type]
    forall {a} {b}. RecordMap a b -> [Field a b]
    mkRec RecordMap Ident Type
    y)
            (TNewtype Newtype
    x [Type]
    xs, TNewtype Newtype
    y [Type]
    ys) -> Field Newtype [Type] -> Field Newtype [Type] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same (Newtype -> [Type] -> Field Newtype [Type]
    forall a b. a -> b -> Field a b
    Field Newtype
    x [Type]
    xs) (Newtype -> [Type] -> Field Newtype [Type]
    forall a b. a -> b -> Field a b
    Field Newtype
    y [Type]
    ys)
            (TCon TCon
    x [Type]
    xs, TCon TCon
    y [Type]
    ys)         -> Field TCon [Type] -> Field TCon [Type] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same (TCon -> [Type] -> Field TCon [Type]
    forall a b. a -> b -> Field a b
    Field TCon
    x [Type]
    xs) (TCon -> [Type] -> Field TCon [Type]
    forall a b. a -> b -> Field a b
    Field TCon
    y [Type]
    ys)
            (Type, Type)
    _                              -> AreSame
    NotSame
          where
          k1 :: Kind
    k1 = Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t1
          k2 :: Kind
    k2 = Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t2
          mkRec :: RecordMap a b -> [Field a b]
    mkRec RecordMap a b
    r = [ a -> b -> Field a b
    forall a b. a -> b -> Field a b
    Field a
    x b
    y | (a
    x,b
    y) <- RecordMap a b -> [(a, b)]
    forall a b. RecordMap a b -> [(a, b)]
    canonicalFields RecordMap a b
    r ]

    instance Same Schema where
      same :: Schema -> Schema -> AreSame
    same (Forall [TParam]
    xs [Type]
    ps Type
    s) (Forall [TParam]
    ys [Type]
    qs Type
    t) =
        [TParam] -> [TParam] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same [TParam]
    xs [TParam]
    ys AreSame -> AreSame -> AreSame
    `sameAnd` [Type] -> [Type] -> AreSame
    forall a. Same a => a -> a -> AreSame
    same [Type]
    ps [Type]
    qs AreSame -> AreSame -> AreSame
    `sameAnd` Type -> Type -> AreSame
    forall a. Same a => a -> a -> AreSame
    same Type
    s Type
    t

    instance Same TParam where
      same :: TParam -> TParam -> AreSame
    same TParam
    x TParam
    y = Bool -> AreSame
    sameBool (TParam -> Maybe Name
    tpName TParam
    x Maybe Name -> Maybe Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam -> Maybe Name
    tpName TParam
    y Bool -> Bool -> Bool
    && TParam -> Kind
    tpKind TParam
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam -> Kind
    tpKind TParam
    y)

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

    -- | Check that the expression is well-formed, and compute its type.
    -- Reports an error if the expression is not of a mono type.
    exprType :: Expr -> TcM Type
    exprType :: Expr -> TcM Type
    exprType Expr
    expr =
      do Schema
    s <- Expr -> TcM Schema
    exprSchema Expr
    expr
         case Schema -> Maybe Type
    isMono Schema
    s of
           Just Type
    t  -> Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
           Maybe Type
    Nothing -> Error -> TcM Type
    forall a. Error -> TcM a
    reportError (Schema -> Error
    ExpectedMono Schema
    s)

    -- | Check that the expression is well-formed, and compute its schema.
    exprSchema :: Expr -> TcM Schema
    exprSchema :: Expr -> TcM Schema
    exprSchema Expr
    expr =
      case Expr
    expr of

        ELocated Range
    rng Expr
    t -> Range -> TcM Schema -> TcM Schema
    forall a. Range -> TcM a -> TcM a
    withRange Range
    rng (Expr -> TcM Schema
    exprSchema Expr
    t)

        EList [Expr]
    es Type
    t ->
          do Kind -> Type -> TcM ()
    checkTypeIs Kind
    KType Type
    t
             [Expr] -> (Expr -> TcM ()) -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Expr]
    es ((Expr -> TcM ()) -> TcM ()) -> (Expr -> TcM ()) -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ \Expr
    e ->
               do Type
    t1 <- Expr -> TcM Type
    exprType Expr
    e
                  String -> Type -> Type -> TcM ()
    sameTypes String
    "EList" Type
    t1 Type
    t

             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Schema
    tMono (Type -> Schema) -> Type -> Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    tSeq (Int -> Type
    forall a. Integral a => a -> Type
    tNum ([Expr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Expr]
    es)) Type
    t

        ETuple [Expr]
    es ->
          ([Type] -> Schema) -> TcM [Type] -> TcM Schema
    forall a b. (a -> b) -> TcM a -> TcM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Type -> Schema
    tMono (Type -> Schema) -> ([Type] -> Type) -> [Type] -> Schema
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Type] -> Type
    tTuple) ((Expr -> TcM Type) -> [Expr] -> TcM [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Expr -> TcM Type
    exprType [Expr]
    es)

        ERec RecordMap Ident Expr
    fs ->
          do RecordMap Ident Type
    fs1 <- (Expr -> TcM Type)
    -> RecordMap Ident Expr -> TcM (RecordMap Ident Type)
    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) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse Expr -> TcM Type
    exprType RecordMap Ident Expr
    fs
             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Schema
    tMono (Type -> Schema) -> Type -> Schema
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident Type -> Type
    TRec RecordMap Ident Type
    fs1

        ESet Type
    _ Expr
    e Selector
    x Expr
    v ->
           do Type
    ty  <- Expr -> TcM Type
    exprType Expr
    e
              Type
    expe <- Type -> Selector -> TcM Type
    checkHas Type
    ty Selector
    x
              Type
    has <- Expr -> TcM Type
    exprType Expr
    v
              String -> Type -> Type -> TcM ()
    sameTypes String
    "ESet" Type
    expe Type
    has
              Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Schema
    tMono Type
    ty)

        ESel Expr
    e Selector
    sel -> do Type
    ty <- Expr -> TcM Type
    exprType Expr
    e
                         Type
    ty1 <- Type -> Selector -> TcM Type
    checkHas Type
    ty Selector
    sel
                         Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Schema
    tMono Type
    ty1)

        EIf Expr
    e1 Expr
    e2 Expr
    e3 ->
          do Type
    ty <- Expr -> TcM Type
    exprType Expr
    e1
             String -> Type -> Type -> TcM ()
    sameTypes String
    "EIf_condition" Type
    tBit Type
    ty

             Type
    t1 <- Expr -> TcM Type
    exprType Expr
    e2
             Type
    t2 <- Expr -> TcM Type
    exprType Expr
    e3
             String -> Type -> Type -> TcM ()
    sameTypes String
    "EIf_arms" Type
    t1 Type
    t2

             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Schema
    tMono Type
    t1

        EComp Type
    len Type
    t Expr
    e [[Match]]
    mss ->
          do Kind -> Type -> TcM ()
    checkTypeIs Kind
    KNum Type
    len
             Kind -> Type -> TcM ()
    checkTypeIs Kind
    KType Type
    t

             ([[(Name, Schema)]]
    xs,[Type]
    ls) <- [([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([([(Name, Schema)], Type)] -> ([[(Name, Schema)]], [Type]))
    -> TcM [([(Name, Schema)], Type)]
    -> TcM ([[(Name, Schema)]], [Type])
    forall a b. (a -> b) -> TcM a -> TcM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` ([Match] -> TcM ([(Name, Schema)], Type))
    -> [[Match]] -> TcM [([(Name, Schema)], Type)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM [Match] -> TcM ([(Name, Schema)], Type)
    checkArm [[Match]]
    mss
             -- XXX: check no duplicates
             Type
    elT <- [(Name, Schema)] -> TcM Type -> TcM Type
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars ([[(Name, Schema)]] -> [(Name, Schema)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(Name, Schema)]]
    xs) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ Expr -> TcM Type
    exprType Expr
    e

             case [Type]
    ls of
               [] -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
               [Type]
    _  -> Type -> Type -> TcM ()
    convertible (Type -> Type -> Type
    tSeq Type
    len Type
    t) (Type -> Type -> Type
    tSeq ((Type -> Type -> Type) -> [Type] -> Type
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Type -> Type -> Type
    tMin [Type]
    ls) Type
    elT)

             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Schema
    tMono (Type -> Type -> Type
    tSeq Type
    len Type
    t))

        EVar Name
    x -> Name -> TcM Schema
    lookupVar Name
    x

        ETAbs TParam
    a Expr
    e     ->
          do Forall [TParam]
    as [Type]
    p Type
    t <- TParam -> TcM Schema -> TcM Schema
    forall a. TParam -> TcM a -> TcM a
    withTVar TParam
    a (Expr -> TcM Schema
    exprSchema Expr
    e)
             Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((TParam -> Bool) -> [TParam] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (TParam -> TParam -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam
    a) [TParam]
    as) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $
               Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ TParam -> Error
    RepeatedVariableInForall TParam
    a

             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam] -> [Type] -> Type -> Schema
    Forall (TParam
    a TParam -> [TParam] -> [TParam]
    forall a. a -> [a] -> [a]
    : [TParam]
    as) [Type]
    p Type
    t)

        ETApp Expr
    e Type
    t ->
          do Kind
    k <- Type -> TcM Kind
    checkType Type
    t
             Schema
    s <- Expr -> TcM Schema
    exprSchema Expr
    e
             case Schema
    s of
               Forall (TParam
    a : [TParam]
    as) [Type]
    ps Type
    t1 ->
                 do let vs :: Set TVar
    vs = Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    t

                    [TVar] -> (TVar -> TcM ()) -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar [TParam]
    as) ((TVar -> TcM ()) -> TcM ()) -> (TVar -> TcM ()) -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ \TVar
    b ->
                      Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (TVar
    b TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TVar
    vs) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ TVar -> Error
    Captured TVar
    b

                    let k' :: Kind
    k' = TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    a
                    Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Kind
    k Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k') (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch Kind
    k' Kind
    k

                    let su :: Subst
    su = TParam -> Type -> Subst
    singleTParamSubst TParam
    a Type
    t
                    Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ [TParam] -> [Type] -> Type -> Schema
    Forall [TParam]
    as (Subst -> [Type] -> [Type]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Type]
    ps) (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    t1)

               Forall [] [Type]
    _ Type
    _ -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError Error
    BadInstantiation

        EApp Expr
    e1 Expr
    e2 ->
          do Type
    t1 <- Expr -> TcM Type
    exprType Expr
    e1
             Type
    t2 <- Expr -> TcM Type
    exprType Expr
    e2

             case Type -> Type
    tNoUser Type
    t1 of
               TCon (TC TC
    TCFun) [ Type
    a, Type
    b ]
                  | SameIf [Type]
    ps <- Type -> Type -> AreSame
    forall a. Same a => a -> a -> AreSame
    same Type
    a Type
    t2 ->
                    do (Type -> TcM ()) -> [Type] -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Type -> TcM ()
    proofObligation [Type]
    ps
                       Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> Schema
    tMono Type
    b)
               Type
    tf -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError (Type -> Type -> Error
    BadApplication Type
    tf Type
    t1)

        EAbs Name
    x Type
    t Expr
    e    ->
          do Kind -> Type -> TcM ()
    checkTypeIs Kind
    KType Type
    t
             Type
    res <- Name -> Type -> TcM Type -> TcM Type
    forall a. Name -> Type -> TcM a -> TcM a
    withVar Name
    x Type
    t (Expr -> TcM Type
    exprType Expr
    e)
             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Schema
    tMono (Type -> Schema) -> Type -> Schema
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    tFun Type
    t Type
    res

        EProofAbs Type
    p Expr
    e ->
          do Kind -> Type -> TcM ()
    checkTypeIs Kind
    KProp Type
    p
             Type -> TcM Schema -> TcM Schema
    forall a. Type -> TcM a -> TcM a
    withAsmp Type
    p (TcM Schema -> TcM Schema) -> TcM Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ do Forall [TParam]
    as [Type]
    ps Type
    t <- Expr -> TcM Schema
    exprSchema Expr
    e
                             Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ [TParam] -> [Type] -> Type -> Schema
    Forall [TParam]
    as (Type
    p Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : [Type]
    ps) Type
    t

        EProofApp Expr
    e ->
          do Forall [TParam]
    as [Type]
    ps Type
    t <- Expr -> TcM Schema
    exprSchema Expr
    e
             case ([TParam]
    as,[Type]
    ps) of
               ([], Type
    p:[Type]
    qs) -> do Type -> TcM ()
    proofObligation Type
    p
                                Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam] -> [Type] -> Type -> Schema
    Forall [] [Type]
    qs Type
    t)
               ([], [Type]
    _)    -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError Error
    BadProofNoAbs
               ([TParam]
    _,[Type]
    _)      -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError ([TParam] -> Error
    BadProofTyVars [TParam]
    as)

        -- XXX: Check that defined things are distinct?
        EWhere Expr
    e [DeclGroup]
    dgs ->
          let go :: [DeclGroup] -> TcM Schema
    go []       = Expr -> TcM Schema
    exprSchema Expr
    e
              go (DeclGroup
    d : [DeclGroup]
    ds) = do [(Name, Schema)]
    xs <- DeclGroup -> TcM [(Name, Schema)]
    checkDeclGroup DeclGroup
    d
                               [(Name, Schema)] -> TcM Schema -> TcM Schema
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)]
    xs ([DeclGroup] -> TcM Schema
    go [DeclGroup]
    ds)
          in [DeclGroup] -> TcM Schema
    go [DeclGroup]
    dgs

        EPropGuards [([Type], Expr)]
    _guards Type
    typ ->
          Schema -> TcM Schema
    forall a. a -> TcM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Forall {sVars :: [TParam]
    sVars = [], sProps :: [Type]
    sProps = [], sType :: Type
    sType = Type
    typ}

    checkHas :: Type -> Selector -> TcM Type
    checkHas :: Type -> Selector -> TcM Type
    checkHas Type
    t Selector
    sel =
      case Selector
    sel of

        TupleSel Int
    n Maybe Int
    mb ->

          case Type -> Type
    tNoUser Type
    t of
            TCon (TC (TCTuple Int
    sz)) [Type]
    ts ->
              do case Maybe Int
    mb of
                   Just Int
    sz1 ->
                     Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    sz1) (Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Int -> Int -> Error
    UnexpectedTupleShape Int
    sz1 Int
    sz))
                   Maybe Int
    Nothing  -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                 Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    sz) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Int -> Int -> Error
    TupleSelectorOutOfRange Int
    n Int
    sz)
                 Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TcM Type) -> Type -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ [Type]
    ts [Type] -> Int -> Type
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n

            TCon (TC TC
    TCSeq) [Type
    s,Type
    elT] ->
               do Type
    res <- Type -> Selector -> TcM Type
    checkHas Type
    elT Selector
    sel
                  Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Type] -> Type
    TCon (TC -> TCon
    TC TC
    TCSeq) [Type
    s,Type
    res])

            TCon (TC TC
    TCFun) [Type
    a,Type
    b] ->
                do Type
    res <- Type -> Selector -> TcM Type
    checkHas Type
    b Selector
    sel
                   Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Type] -> Type
    TCon (TC -> TCon
    TC TC
    TCFun) [Type
    a,Type
    res])

            Type
    _ -> Error -> TcM Type
    forall a. Error -> TcM a
    reportError (Error -> TcM Type) -> Error -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ Selector -> Type -> Error
    BadSelector Selector
    sel Type
    t

        RecordSel Ident
    f Maybe [Ident]
    mb ->
          case Type -> Type
    tNoUser Type
    t of
            TRec RecordMap Ident Type
    fs ->

              do case Maybe [Ident]
    mb of
                   Maybe [Ident]
    Nothing -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                   Just [Ident]
    fs1 ->
                     do let ns :: [Ident]
    ns  = Set Ident -> [Ident]
    forall a. Set a -> [a]
    Set.toList (RecordMap Ident Type -> Set Ident
    forall a b. Ord a => RecordMap a b -> Set a
    fieldSet RecordMap Ident Type
    fs)
                            ns1 :: [Ident]
    ns1 = [Ident] -> [Ident]
    forall a. Ord a => [a] -> [a]
    sort [Ident]
    fs1
                        Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Ident]
    ns [Ident] -> [Ident] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Ident]
    ns1) (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $
                          Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ [Ident] -> [Ident] -> Error
    UnexpectedRecordShape [Ident]
    ns1 [Ident]
    ns

                 case Ident -> RecordMap Ident Type -> Maybe Type
    forall a b. Ord a => a -> RecordMap a b -> Maybe b
    lookupField Ident
    f RecordMap Ident Type
    fs of
                   Maybe Type
    Nothing -> Error -> TcM Type
    forall a. Error -> TcM a
    reportError (Error -> TcM Type) -> Error -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ Ident -> [Ident] -> Error
    MissingField Ident
    f ([Ident] -> Error) -> [Ident] -> Error
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident Type -> [Ident]
    forall a b. RecordMap a b -> [a]
    displayOrder RecordMap Ident Type
    fs
                   Just Type
    ft -> Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ft

            TCon (TC TC
    TCSeq) [Type
    s,Type
    elT] -> do Type
    res <- Type -> Selector -> TcM Type
    checkHas Type
    elT Selector
    sel
                                          Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Type] -> Type
    TCon (TC -> TCon
    TC TC
    TCSeq) [Type
    s,Type
    res])

            TCon (TC TC
    TCFun) [Type
    a,Type
    b]   -> do Type
    res <- Type -> Selector -> TcM Type
    checkHas Type
    b Selector
    sel
                                          Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TCon -> [Type] -> Type
    TCon (TC -> TCon
    TC TC
    TCFun) [Type
    a,Type
    res])

            Type
    _ -> Error -> TcM Type
    forall a. Error -> TcM a
    reportError (Error -> TcM Type) -> Error -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ Selector -> Type -> Error
    BadSelector Selector
    sel Type
    t

        -- XXX: Remove this?
        ListSel Int
    _ Maybe Int
    mb ->
          case Type -> Type
    tNoUser Type
    t of
            TCon (TC TC
    TCSeq) [ Type
    n, Type
    elT ] ->

              do case Maybe Int
    mb of
                   Maybe Int
    Nothing  -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                   Just Int
    len ->
                     case Type -> Type
    tNoUser Type
    n of
                       TCon (TC (TCNum Integer
    m)) []
                         | Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    len -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                       Type
    _ -> Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Error
    UnexpectedSequenceShape Int
    len Type
    n

                 Type -> TcM Type
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    elT

            Type
    _ -> Error -> TcM Type
    forall a. Error -> TcM a
    reportError (Error -> TcM Type) -> Error -> TcM Type
    forall a b. (a -> b) -> a -> b
    $ Selector -> Type -> Error
    BadSelector Selector
    sel Type
    t

    -- | Check if the one type is convertible to the other.
    convertible :: Type -> Type -> TcM ()
    convertible :: Type -> Type -> TcM ()
    convertible Type
    t1 Type
    t2
      | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Kind
    k2    = Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Kind -> Kind -> Error
    KindMismatch Kind
    k1 Kind
    k2)
      | Kind
    k1 Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    KNum  = Type -> TcM ()
    proofObligation (Type
    t1 Type -> Type -> Type
    =#= Type
    t2)
      where
      k1 :: Kind
    k1 = Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t1
      k2 :: Kind
    k2 = Type -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Type
    t2

    convertible Type
    t1 Type
    t2 = Type -> Type -> TcM ()
    go Type
    t1 Type
    t2
      where
      go :: Type -> Type -> TcM ()
    go Type
    ty1 Type
    ty2 =
        let err :: TcM a
    err   = Error -> TcM a
    forall a. Error -> TcM a
    reportError (Error -> TcM a) -> Error -> TcM a
    forall a b. (a -> b) -> a -> b
    $ String -> Schema -> Schema -> Error
    TypeMismatch String
    "convertible" (Type -> Schema
    tMono Type
    ty1) (Type -> Schema
    tMono Type
    ty2)
            other :: Type
    other = Type -> Type
    tNoUser Type
    ty2

            goMany :: [Type] -> [Type] -> TcM ()
    goMany [] []             = () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            goMany (Type
    x : [Type]
    xs) (Type
    y : [Type]
    ys) = Type -> Type -> TcM ()
    convertible Type
    x Type
    y TcM () -> TcM () -> TcM ()
    forall a b. TcM a -> TcM b -> TcM b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Type] -> [Type] -> TcM ()
    goMany [Type]
    xs [Type]
    ys
            goMany [Type]
    _ [Type]
    _               = TcM ()
    forall {a}. TcM a
    err

        in case Type
    ty1 of
             TUser Name
    _ [Type]
    _ Type
    s   -> Type -> Type -> TcM ()
    go Type
    s Type
    ty2

             TVar TVar
    x        -> case Type
    other of
                                TVar TVar
    y | TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    y  -> () -> TcM ()
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                Type
    _                -> TcM ()
    forall {a}. TcM a
    err

             TCon TCon
    tc1 [Type]
    ts1  -> case Type
    other of
                                TCon TCon
    tc2 [Type]
    ts2
                                   | TCon
    tc1 TCon -> TCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TCon
    tc2 -> [Type] -> [Type] -> TcM ()
    goMany [Type]
    ts1 [Type]
    ts2
                                Type
    _ -> TcM ()
    forall {a}. TcM a
    err

             TNewtype Newtype
    nt1 [Type]
    ts1 ->
                case Type
    other of
                  TNewtype Newtype
    nt2 [Type]
    ts2
                    | Newtype
    nt1 Newtype -> Newtype -> Bool
    forall a. Eq a => a -> a -> Bool
    == Newtype
    nt2 -> [Type] -> [Type] -> TcM ()
    goMany [Type]
    ts1 [Type]
    ts2
                  Type
    _ -> TcM ()
    forall {a}. TcM a
    err

             TRec RecordMap Ident Type
    fs ->
               case Type
    other of
                 TRec RecordMap Ident Type
    gs ->
                   do Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (RecordMap Ident Type -> Set Ident
    forall a b. Ord a => RecordMap a b -> Set a
    fieldSet RecordMap Ident Type
    fs Set Ident -> Set Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    == RecordMap Ident Type -> Set Ident
    forall a b. Ord a => RecordMap a b -> Set a
    fieldSet RecordMap Ident Type
    gs) TcM ()
    forall {a}. TcM a
    err
                      [Type] -> [Type] -> TcM ()
    goMany (RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    fs) (RecordMap Ident Type -> [Type]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident Type
    gs)
                 Type
    _ -> TcM ()
    forall {a}. TcM a
    err

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

    -- | Check a declaration. The boolean indicates if we should check the siganture
    checkDecl :: Bool -> Decl -> TcM (Name, Schema)
    checkDecl :: Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    checkSig Decl
    d =
      case Decl -> DeclDef
    dDefinition Decl
    d of

        DeclDef
    DPrim ->
          do Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Schema -> TcM ()
    checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Decl -> Schema
    dSignature Decl
    d
             (Name, Schema) -> TcM (Name, Schema)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> Name
    dName Decl
    d, Decl -> Schema
    dSignature Decl
    d)

        DForeign FFIFunType
    _ ->
          do Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Schema -> TcM ()
    checkSchema (Schema -> TcM ()) -> Schema -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Decl -> Schema
    dSignature Decl
    d
             (Name, Schema) -> TcM (Name, Schema)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> Name
    dName Decl
    d, Decl -> Schema
    dSignature Decl
    d)

        DExpr Expr
    e ->
          do let s :: Schema
    s = Decl -> Schema
    dSignature Decl
    d
             Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    checkSig (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Schema -> TcM ()
    checkSchema Schema
    s
             Schema
    s1 <- Expr -> TcM Schema
    exprSchema Expr
    e
             let nm :: Name
    nm = Decl -> Name
    dName Decl
    d
                 loc :: String
    loc = String
    "definition of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    nm) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                                String
    ", at " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Range -> Doc
    forall a. PP a => a -> Doc
    pp (Name -> Range
    nameLoc Name
    nm))
             String -> Schema -> Schema -> TcM ()
    sameSchemas String
    loc Schema
    s Schema
    s1

             (Name, Schema) -> TcM (Name, Schema)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> Name
    dName Decl
    d, Schema
    s)

    checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
    checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
    checkDeclGroup DeclGroup
    dg =
      case DeclGroup
    dg of
        NonRecursive Decl
    d -> do (Name, Schema)
    x <- Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    True Decl
    d
                             [(Name, Schema)] -> TcM [(Name, Schema)]
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Name, Schema)
    x]
        Recursive [Decl]
    ds ->
          do [(Name, Schema)]
    xs <- [Decl] -> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Decl]
    ds ((Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)])
    -> (Decl -> TcM (Name, Schema)) -> TcM [(Name, Schema)]
    forall a b. (a -> b) -> a -> b
    $ \Decl
    d ->
                      do Schema -> TcM ()
    checkSchema (Decl -> Schema
    dSignature Decl
    d)
                         (Name, Schema) -> TcM (Name, Schema)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> Name
    dName Decl
    d, Decl -> Schema
    dSignature Decl
    d)
             [(Name, Schema)] -> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)]
    xs (TcM [(Name, Schema)] -> TcM [(Name, Schema)])
    -> TcM [(Name, Schema)] -> TcM [(Name, Schema)]
    forall a b. (a -> b) -> a -> b
    $ (Decl -> TcM (Name, Schema)) -> [Decl] -> TcM [(Name, Schema)]
    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 (Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    False) [Decl]
    ds

    checkMatch :: Match -> TcM ((Name, Schema), Type)
    checkMatch :: Match -> TcM ((Name, Schema), Type)
    checkMatch Match
    ma =
      case Match
    ma of
        From Name
    x Type
    len Type
    elt Expr
    e ->
          do Kind -> Type -> TcM ()
    checkTypeIs Kind
    KNum Type
    len
             Kind -> Type -> TcM ()
    checkTypeIs Kind
    KType Type
    elt
             Type
    t1 <- Expr -> TcM Type
    exprType Expr
    e
             case Type -> Type
    tNoUser Type
    t1 of
               TCon (TC TC
    TCSeq) [ Type
    l, Type
    el ]
                 | SameIf [Type]
    ps <- Type -> Type -> AreSame
    forall a. Same a => a -> a -> AreSame
    same Type
    elt Type
    el ->
                   do (Type -> TcM ()) -> [Type] -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Type -> TcM ()
    proofObligation [Type]
    ps
                      ((Name, Schema), Type) -> TcM ((Name, Schema), Type)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Name
    x, Type -> Schema
    tMono Type
    elt), Type
    l)
                 | Bool
    otherwise -> Error -> TcM ((Name, Schema), Type)
    forall a. Error -> TcM a
    reportError (Error -> TcM ((Name, Schema), Type))
    -> Error -> TcM ((Name, Schema), Type)
    forall a b. (a -> b) -> a -> b
    $ String -> Schema -> Schema -> Error
    TypeMismatch String
    "From" (Type -> Schema
    tMono Type
    elt) (Type -> Schema
    tMono Type
    el)

               Type
    _ -> Error -> TcM ((Name, Schema), Type)
    forall a. Error -> TcM a
    reportError (Error -> TcM ((Name, Schema), Type))
    -> Error -> TcM ((Name, Schema), Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Error
    BadMatch Type
    t1

        Let Decl
    d -> do (Name, Schema)
    x <- Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    True Decl
    d
                    ((Name, Schema), Type) -> TcM ((Name, Schema), Type)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Name, Schema)
    x, Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    1 :: Int))

    checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
    checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
    checkArm []   = Error -> TcM ([(Name, Schema)], Type)
    forall a. Error -> TcM a
    reportError Error
    EmptyArm
    checkArm [Match
    m]  = do ((Name, Schema)
    x,Type
    l) <- Match -> TcM ((Name, Schema), Type)
    checkMatch Match
    m
                       ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Name, Schema)
    x], Type
    l)
    checkArm (Match
    m : [Match]
    ms) =
      do ((Name, Schema)
    x, Type
    l)   <- Match -> TcM ((Name, Schema), Type)
    checkMatch Match
    m
         ([(Name, Schema)]
    xs, Type
    l1) <- [(Name, Schema)]
    -> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)
    x] (TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
    -> TcM ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
    forall a b. (a -> b) -> a -> b
    $ [Match] -> TcM ([(Name, Schema)], Type)
    checkArm [Match]
    ms
         let newLen :: Type
    newLen = Type -> Type -> Type
    tMul Type
    l Type
    l1
         ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type))
    -> ([(Name, Schema)], Type) -> TcM ([(Name, Schema)], Type)
    forall a b. (a -> b) -> a -> b
    $ if (Name, Schema) -> Name
    forall a b. (a, b) -> a
    fst (Name, Schema)
    x Name -> [Name] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Name, Schema) -> Name) -> [(Name, Schema)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Schema) -> Name
    forall a b. (a, b) -> a
    fst [(Name, Schema)]
    xs
                     then ([(Name, Schema)]
    xs, Type
    newLen)
                     else ((Name, Schema)
    x (Name, Schema) -> [(Name, Schema)] -> [(Name, Schema)]
    forall a. a -> [a] -> [a]
    : [(Name, Schema)]
    xs, Type
    newLen)

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

    data RO = RO
      { RO -> Map Int TParam
    roTVars   :: Map Int TParam
      , RO -> [Type]
    roAsmps   :: [Prop]
      , RO -> Range
    roRange   :: Range
      , RO -> Map Name Schema
    roVars    :: Map Name Schema
      }

    type ProofObligation = Schema -- but the type is of kind Prop

    data RW = RW
      { RW -> [Schema]
    woProofObligations :: [ProofObligation]
      }

    newtype TcM a = TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a)

    instance Functor TcM where
      fmap :: forall a b. (a -> b) -> TcM a -> TcM b
    fmap = (a -> b) -> TcM a -> TcM b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance A.Applicative TcM where
      pure :: forall a. a -> TcM a
    pure a
    a = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    a -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a)
      <*> :: forall a b. TcM (a -> b) -> TcM a -> TcM b
    (<*>) = TcM (a -> b) -> TcM a -> TcM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad TcM where
      return :: forall a. a -> TcM a
    return      = a -> TcM a
    forall a. a -> TcM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m >>= :: forall a b. TcM a -> (a -> TcM b) -> TcM b
    >>= a -> TcM b
    f = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b -> TcM b
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (do a
    a <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m
                            let TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
    m1 = a -> TcM b
    f a
    a
                            ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) b
    m1)

    runTcM :: InferInput -> TcM a -> Either (Range, Error) (a, [ProofObligation])
    runTcM :: forall a.
    InferInput -> TcM a -> Either (Range, Error) (a, [Schema])
    runTcM InferInput
    env (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m) =
      case ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> RO -> RW -> (Either (Range, Error) a, RW)
    forall (m :: * -> *) a r. RunM m a r => m a -> r
    runM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m RO
    ro RW
    rw of
        (Left (Range, Error)
    err, RW
    _) -> (Range, Error) -> Either (Range, Error) (a, [Schema])
    forall a b. a -> Either a b
    Left (Range, Error)
    err
        (Right a
    a, RW
    s)  -> (a, [Schema]) -> Either (Range, Error) (a, [Schema])
    forall a b. b -> Either a b
    Right (a
    a, RW -> [Schema]
    woProofObligations RW
    s)
      where
      allPs :: ModParamNames
    allPs = InferInput -> ModParamNames
    inpParams InferInput
    env

      ro :: RO
    ro = RO { roTVars :: Map Int TParam
    roTVars = [(Int, TParam)] -> Map Int TParam
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (TParam -> Int
    tpUnique TParam
    x, TParam
    x)
                                          | ModTParam
    tp <- Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems (ModParamNames -> Map Name ModTParam
    mpnTypes ModParamNames
    allPs)
                                          , let x :: TParam
    x = ModTParam -> TParam
    mtpParam ModTParam
    tp ]
              , roAsmps :: [Type]
    roAsmps = (Located Type -> Type) -> [Located Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Type -> Type
    forall a. Located a -> a
    thing (ModParamNames -> [Located Type]
    mpnConstraints ModParamNames
    allPs)
              , roRange :: Range
    roRange = Range
    emptyRange
              , roVars :: Map Name Schema
    roVars  = Map Name Schema -> Map Name Schema -> Map Name Schema
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union
                            ((ModVParam -> Schema) -> Map Name ModVParam -> Map Name Schema
    forall a b. (a -> b) -> Map Name a -> Map Name b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModVParam -> Schema
    mvpType (ModParamNames -> Map Name ModVParam
    mpnFuns ModParamNames
    allPs))
                            (InferInput -> Map Name Schema
    inpVars InferInput
    env)
              }
      rw :: RW
    rw = RW { woProofObligations :: [Schema]
    woProofObligations = [] }

    data Error =
        TypeMismatch String Schema Schema    -- ^ expected, actual
      | ExpectedMono Schema           -- ^ expected a mono type, got this
      | TupleSelectorOutOfRange Int Int
      | MissingField Ident [Ident]
      | UnexpectedTupleShape Int Int
      | UnexpectedRecordShape [Ident] [Ident]
      | UnexpectedSequenceShape Int Type
      | BadSelector Selector Type
      | BadInstantiation
      | Captured TVar
      | BadProofNoAbs
      | BadProofTyVars [TParam]
      | KindMismatch Kind Kind
      | NotEnoughArgumentsInKind Kind
      | BadApplication Type Type
      | FreeTypeVariable TVar
      | BadTypeApplication Kind [Kind]
      | RepeatedVariableInForall TParam
      | BadMatch Type
      | EmptyArm
      | UndefinedTypeVaraible TVar
      | UndefinedVariable Name
        deriving Int -> Error -> String -> String
    [Error] -> String -> String
    Error -> String
    (Int -> Error -> String -> String)
    -> (Error -> String) -> ([Error] -> String -> String) -> Show Error
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> Error -> String -> String
    showsPrec :: Int -> Error -> String -> String
    $cshow :: Error -> String
    show :: Error -> String
    $cshowList :: [Error] -> String -> String
    showList :: [Error] -> String -> String
    Show

    reportError :: Error -> TcM a
    reportError :: forall a. Error -> TcM a
    reportError Error
    e = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         (Range, Error)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    (Range, Error)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise (RO -> Range
    roRange RO
    ro, Error
    e)

    withTVar :: TParam -> TcM a -> TcM a
    withTVar :: forall a. TParam -> TcM a -> TcM a
    withTVar TParam
    a (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local RO
    ro { roTVars :: Map Int TParam
    roTVars = Int -> TParam -> Map Int TParam -> Map Int TParam
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (TParam -> Int
    tpUnique TParam
    a) TParam
    a (RO -> Map Int TParam
    roTVars RO
    ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m

    withRange :: Range -> TcM a -> TcM a
    withRange :: forall a. Range -> TcM a -> TcM a
    withRange Range
    rng (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local RO
    ro { roRange :: Range
    roRange = Range
    rng } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m

    withAsmp :: Prop -> TcM a -> TcM a
    withAsmp :: forall a. Type -> TcM a -> TcM a
    withAsmp Type
    p (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local RO
    ro { roAsmps :: [Type]
    roAsmps = Type
    p Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    : RO -> [Type]
    roAsmps RO
    ro } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m

    withVar :: Name -> Type -> TcM a -> TcM a
    withVar :: forall a. Name -> Type -> TcM a -> TcM a
    withVar Name
    x Type
    t = [(Name, Schema)] -> TcM a -> TcM a
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name
    x,Type -> Schema
    tMono Type
    t)]

    withVars :: [(Name, Schema)] -> TcM a -> TcM a
    withVars :: forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)]
    xs (TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall a.
    RO
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local RO
    ro { roVars :: Map Name Schema
    roVars = Map Name Schema -> Map Name Schema -> Map Name Schema
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union ([(Name, Schema)] -> Map Name Schema
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, Schema)]
    xs) (RO -> Map Name Schema
    roVars RO
    ro) } ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a
    m

    proofObligation :: Prop -> TcM ()
    proofObligation :: Type -> TcM ()
    proofObligation Type
    p = ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) () -> TcM ()
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
     -> TcM ())
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
    -> TcM ()
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         (RW -> RW)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
    forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
    sets_ ((RW -> RW)
     -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ())
    -> (RW -> RW)
    -> ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    rw -> RW
    rw { woProofObligations :: [Schema]
    woProofObligations =
                                 [TParam] -> [Type] -> Type -> Schema
    Forall (Map Int TParam -> [TParam]
    forall k a. Map k a -> [a]
    Map.elems (RO -> Map Int TParam
    roTVars RO
    ro)) (RO -> [Type]
    roAsmps RO
    ro) Type
    p
                               Schema -> [Schema] -> [Schema]
    forall a. a -> [a] -> [a]
    : RW -> [Schema]
    woProofObligations RW
    rw }

    lookupTVar :: TVar -> TcM Kind
    lookupTVar :: TVar -> TcM Kind
    lookupTVar TVar
    x =
      case TVar
    x of
        TVFree {} -> Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (TVar -> Error
    FreeTypeVariable TVar
    x)
        TVBound TParam
    tpv ->
           do let u :: Int
    u = TParam -> Int
    tpUnique TParam
    tpv
                  k :: Kind
    k = TParam -> Kind
    tpKind TParam
    tpv
              RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
              case Int -> Map Int TParam -> Maybe TParam
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Int
    u (RO -> Map Int TParam
    roTVars RO
    ro) of
                Just TParam
    tp
                  | TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    tp Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k  -> Kind -> TcM Kind
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
                  | Bool
    otherwise       -> Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (Error -> TcM Kind) -> Error -> TcM Kind
    forall a b. (a -> b) -> a -> b
    $ Kind -> Kind -> Error
    KindMismatch (TParam -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TParam
    tp) Kind
    k
                Maybe TParam
    Nothing  -> Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (Error -> TcM Kind) -> Error -> TcM Kind
    forall a b. (a -> b) -> a -> b
    $ TVar -> Error
    UndefinedTypeVaraible TVar
    x

    lookupVar :: Name -> TcM Schema
    lookupVar :: Name -> TcM Schema
    lookupVar Name
    x =
      do RO
    ro <- ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO -> TcM RO
    forall a.
    ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) a -> TcM a
    TcM ReaderT RO (ExceptionT (Range, Error) (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         case Name -> Map Name Schema -> Maybe Schema
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (RO -> Map Name Schema
    roVars RO
    ro) of
           Just Schema
    s -> Schema -> TcM Schema
    forall a. a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Schema
    s
           Maybe Schema
    Nothing -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError (Error -> TcM Schema) -> Error -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Name -> Error
    UndefinedVariable Name
    x

    instance PP Error where
      ppPrec :: Int -> Error -> Doc
    ppPrec Int
    _ Error
    err =
        case Error
    err of

          TypeMismatch String
    what Schema
    expected Schema
    actual ->
            Doc -> [Doc] -> Doc
    ppErr (Doc
    "Type mismatch in" Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    what)
              [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    expected
              , Doc
    "Actual  :" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    actual
              ]

          ExpectedMono Schema
    s ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Not a monomorphic type"
              [ Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    s ]

          TupleSelectorOutOfRange Int
    sel Int
    sz ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Tuple selector out of range"
              [ Doc
    "Selector:" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    sel
              , Doc
    "Size    :" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    sz
              ]

          MissingField Ident
    f [Ident]
    fs ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Invalid record selector"
              [ Doc
    "Field: " Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    f
              , Doc
    "Fields:" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Ident -> Doc
    forall a. PP a => a -> Doc
    pp [Ident]
    fs)
              ]

          UnexpectedTupleShape Int
    expected Int
    actual ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Unexpected tuple shape"
              [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    expected
              , Doc
    "Actual  :" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    actual
              ]

          UnexpectedRecordShape [Ident]
    expected [Ident]
    actual ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Unexpected record shape"
              [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Ident -> Doc
    forall a. PP a => a -> Doc
    pp [Ident]
    expected)
              , Doc
    "Actual  :" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((Ident -> Doc) -> [Ident] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Ident -> Doc
    forall a. PP a => a -> Doc
    pp [Ident]
    actual)
              ]

          UnexpectedSequenceShape Int
    n Type
    t ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Unexpected sequence shape"
              [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> Int -> Doc
    int Int
    n
              , Doc
    "Actual  :" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t
              ]

          BadSelector Selector
    sel Type
    t ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Bad selector"
              [ Doc
    "Selector:" Doc -> Doc -> Doc
    <+> Selector -> Doc
    forall a. PP a => a -> Doc
    pp Selector
    sel
              , Doc
    "Type    :" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t
              ]

          Error
    BadInstantiation ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Bad instantiation" []

          Captured TVar
    x ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Captured type variable"
              [ Doc
    "Variable:" Doc -> Doc -> Doc
    <+> TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    x ]

          Error
    BadProofNoAbs ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Proof application without a proof abstraction" []

          BadProofTyVars [TParam]
    xs ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Proof application with type abstraction"
              [ Doc
    "Type parameter:" Doc -> Doc -> Doc
    <+> TParam -> Doc
    forall a. PP a => a -> Doc
    pp TParam
    x | TParam
    x <- [TParam]
    xs ]

          KindMismatch Kind
    expected Kind
    actual ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Kind mismatch"
              [ Doc
    "Expected:" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    expected
              , Doc
    "Actual  :" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    actual
              ]

          NotEnoughArgumentsInKind Kind
    k ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Not enough arguments in kind" [ Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k ]

          BadApplication Type
    t1 Type
    t2 ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Bad application"
              [ Doc
    "Function:" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t1
              , Doc
    "Argument:" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t2
              ]

          FreeTypeVariable TVar
    x ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Free type variable"
              [ Doc
    "Variable:" Doc -> Doc -> Doc
    <+> TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    x ]

          BadTypeApplication Kind
    kf [Kind]
    ka ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Bad type application"
              [ Doc
    "Function :" Doc -> Doc -> Doc
    <+> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    kf
              , Doc
    "Arguments:" Doc -> Doc -> Doc
    <+> [Doc] -> Doc
    commaSep ((Kind -> Doc) -> [Kind] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> Doc
    forall a. PP a => a -> Doc
    pp [Kind]
    ka)
              ]

          RepeatedVariableInForall TParam
    x ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Repeated variable in forall"
              [ Doc
    "Variable:" Doc -> Doc -> Doc
    <+> TParam -> Doc
    forall a. PP a => a -> Doc
    pp TParam
    x ]

          BadMatch Type
    t ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Bad match"
              [ Doc
    "Type:" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t ]

          Error
    EmptyArm -> Doc -> [Doc] -> Doc
    ppErr Doc
    "Empty comprehension arm" []

          UndefinedTypeVaraible TVar
    x ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Undefined type variable"
              [ Doc
    "Variable:" Doc -> Doc -> Doc
    <+> TVar -> Doc
    forall a. PP a => a -> Doc
    pp TVar
    x ]

          UndefinedVariable Name
    x ->
            Doc -> [Doc] -> Doc
    ppErr Doc
    "Undefined variable"
              [ Doc
    "Variable:" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    x ]

        where
        ppErr :: Doc -> [Doc] -> Doc
    ppErr Doc
    x [Doc]
    ys = Doc -> Int -> Doc -> Doc
    hang Doc
    x Int
    2 ([Doc] -> Doc
    vcat [ Doc
    "•" Doc -> Doc -> Doc
    <+> Doc
    y | Doc
    y <- [Doc]
    ys ])