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

    import Cryptol.Parser.Position(thing)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Subst (apSubst, singleSubst)
    import Cryptol.TypeCheck.Monad(InferInput(..))
    import Cryptol.Utils.Ident

    import qualified Data.Set as Set
    import Data.List (sort, sortBy)
    import Data.Function (on)
    import MonadLib
    import qualified Control.Applicative as A

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

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

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

    tcModule :: InferInput -> Module -> Either Error [ ProofObligation ]
    tcModule :: InferInput -> Module -> Either Error [Schema]
    tcModule env :: InferInput
    env m :: Module
    m = case InferInput -> TcM () -> Either Error ((), [Schema])
    forall a. InferInput -> TcM a -> Either Error (a, [Schema])
    runTcM InferInput
    env TcM ()
    check of
                       Left err :: Error
    err -> Error -> Either Error [Schema]
    forall a b. a -> Either a b
    Left Error
    err
                       Right (_,ps :: [Schema]
    ps) -> [Schema] -> Either Error [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    ps
      where check :: TcM ()
    check = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
    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
    mParamTypes Module
    m)))
            k1 :: TcM ()
    k1    = (Prop -> TcM () -> TcM ()) -> TcM () -> [Prop] -> TcM ()
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> TcM () -> TcM ()
    forall a. Prop -> TcM a -> TcM a
    withAsmp TcM ()
    k2 ((Located Prop -> Prop) -> [Located Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Prop -> Prop
    forall a. Located a -> a
    thing (Module -> [Located Prop]
    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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModVParam -> Schema
    mvpType (Module -> Map Name ModVParam
    mParamFuns Module
    m)))
                  (TcM () -> TcM ()) -> TcM () -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ [DeclGroup] -> TcM ()
    checkDecls (Module -> [DeclGroup]
    mDecls Module
    m)

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

    checkDecls :: [DeclGroup] -> TcM ()
    checkDecls :: [DeclGroup] -> TcM ()
    checkDecls decls :: [DeclGroup]
    decls =
      case [DeclGroup]
    decls of
        [] -> () -> TcM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        d :: DeclGroup
    d : ds :: [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 :: Prop -> TcM Kind
    checkType ty :: Prop
    ty =
      case Prop
    ty of
        TUser _ _ t :: Prop
    t -> Prop -> TcM Kind
    checkType Prop
    t    -- Maybe check synonym too?

        TCon tc :: TCon
    tc ts :: [Prop]
    ts ->
          do [Kind]
    ks <- (Prop -> TcM Kind) -> [Prop] -> TcM [Kind]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Prop -> TcM Kind
    checkType [Prop]
    ts
             Kind -> [Kind] -> TcM Kind
    checkKind (TCon -> Kind
    forall t. HasKind t => t -> Kind
    kindOf TCon
    tc) [Kind]
    ks

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

        TRec fs :: [(Ident, Prop)]
    fs ->
          do [(Ident, Prop)] -> ((Ident, Prop) -> TcM ()) -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(Ident, Prop)]
    fs (((Ident, Prop) -> TcM ()) -> TcM ())
    -> ((Ident, Prop) -> TcM ()) -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ \(_,t :: Prop
    t) ->
               do Kind
    k <- Prop -> TcM Kind
    checkType Prop
    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 (m :: * -> *) a. Monad m => a -> m a
    return Kind
    KType

      where
      checkKind :: Kind -> [Kind] -> TcM Kind
    checkKind k :: Kind
    k [] = case Kind
    k of
                         _ :-> _  -> 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
                         KProp    -> Kind -> TcM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
                         KNum     -> Kind -> TcM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k
                         KType    -> Kind -> TcM Kind
    forall (m :: * -> *) a. Monad m => a -> m a
    return Kind
    k

      checkKind (k1 :: Kind
    k1 :-> k2 :: Kind
    k2) (k :: Kind
    k : ks :: [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 k :: Kind
    k ks :: [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 -> Prop -> TcM ()
    checkTypeIs k :: Kind
    k ty :: Prop
    ty =
      do Kind
    k1 <- Prop -> TcM Kind
    checkType Prop
    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 as :: [TParam]
    as ps :: [Prop]
    ps t :: Prop
    t) = (TParam -> TcM () -> TcM ()) -> TcM () -> [TParam] -> TcM ()
    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 (Prop -> TcM ()) -> [Prop] -> TcM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Kind -> Prop -> TcM ()
    checkTypeIs Kind
    KProp) [Prop]
    ps
                       Kind -> Prop -> TcM ()
    checkTypeIs Kind
    KType Prop
    t

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

    instance Same a => Same [a] where
      same :: [a] -> [a] -> Bool
    same [] [] = Bool
    True
      same (x :: a
    x : xs :: [a]
    xs) (y :: a
    y : ys :: [a]
    ys) = a -> a -> Bool
    forall a. Same a => a -> a -> Bool
    same a
    x a
    y Bool -> Bool -> Bool
    && [a] -> [a] -> Bool
    forall a. Same a => a -> a -> Bool
    same [a]
    xs [a]
    ys
      same _ _ = Bool
    False

    instance Same Type where
      same :: Prop -> Prop -> Bool
    same t1 :: Prop
    t1 t2 :: Prop
    t2 = Prop -> Prop
    tNoUser Prop
    t1 Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    == Prop -> Prop
    tNoUser Prop
    t2

    instance Same Schema where
      same :: Schema -> Schema -> Bool
    same (Forall xs :: [TParam]
    xs ps :: [Prop]
    ps s :: Prop
    s) (Forall ys :: [TParam]
    ys qs :: [Prop]
    qs t :: Prop
    t) = [TParam] -> [TParam] -> Bool
    forall a. Same a => a -> a -> Bool
    same [TParam]
    xs [TParam]
    ys Bool -> Bool -> Bool
    && [Prop] -> [Prop] -> Bool
    forall a. Same a => a -> a -> Bool
    same [Prop]
    ps [Prop]
    qs Bool -> Bool -> Bool
    && Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    s Prop
    t

    instance Same TParam where
      same :: TParam -> TParam -> Bool
    same x :: TParam
    x y :: TParam
    y = 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 Prop
    exprType expr :: Expr
    expr =
      do Schema
    s <- Expr -> TcM Schema
    exprSchema Expr
    expr
         case Schema -> Maybe Prop
    isMono Schema
    s of
           Just t :: Prop
    t  -> Prop -> TcM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    t
           Nothing -> Error -> TcM Prop
    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
    expr =
      case Expr
    expr of

        EList es :: [Expr]
    es t :: Prop
    t ->
          do Kind -> Prop -> TcM ()
    checkTypeIs Kind
    KType Prop
    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
    $ \e :: Expr
    e ->
               do Prop
    t1 <- Expr -> TcM Prop
    exprType Expr
    e
                  Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    t1 Prop
    t) (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
    $ String -> Schema -> Schema -> Error
    TypeMismatch "EList" (Prop -> Schema
    tMono Prop
    t) (Prop -> Schema
    tMono Prop
    t1)

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

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

        ERec fs :: [(Ident, Expr)]
    fs ->
          do [(Ident, Prop)]
    fs1 <- [(Ident, Expr)]
    -> ((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Ident, Expr)]
    fs (((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)])
    -> ((Ident, Expr) -> TcM (Ident, Prop)) -> TcM [(Ident, Prop)]
    forall a b. (a -> b) -> a -> b
    $ \(f :: Ident
    f,e :: Expr
    e) -> do Prop
    t <- Expr -> TcM Prop
    exprType Expr
    e
                                           (Ident, Prop) -> TcM (Ident, Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ident
    f,Prop
    t)
             Schema -> TcM Schema
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ Prop -> Schema
    tMono (Prop -> Schema) -> Prop -> Schema
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Prop)] -> Prop
    TRec [(Ident, Prop)]
    fs1

        ESet e :: Expr
    e x :: Selector
    x v :: Expr
    v -> do Prop
    ty  <- Expr -> TcM Prop
    exprType Expr
    e
                         Prop
    expe <- Prop -> Selector -> TcM Prop
    checkHas Prop
    ty Selector
    x
                         Prop
    has <- Expr -> TcM Prop
    exprType Expr
    v
                         Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    expe Prop
    has) (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
    $
                              String -> Schema -> Schema -> Error
    TypeMismatch "ESet" (Prop -> Schema
    tMono Prop
    expe) (Prop -> Schema
    tMono Prop
    has)
                         Schema -> TcM Schema
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Schema
    tMono Prop
    ty)

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

        EIf e1 :: Expr
    e1 e2 :: Expr
    e2 e3 :: Expr
    e3 ->
          do Prop
    ty <- Expr -> TcM Prop
    exprType Expr
    e1
             Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    tBit Prop
    ty) (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
    $ String -> Schema -> Schema -> Error
    TypeMismatch "EIf_condition" (Prop -> Schema
    tMono Prop
    tBit) (Prop -> Schema
    tMono Prop
    ty)

             Prop
    t1 <- Expr -> TcM Prop
    exprType Expr
    e2
             Prop
    t2 <- Expr -> TcM Prop
    exprType Expr
    e3
             Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    t1 Prop
    t2) (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
    $ String -> Schema -> Schema -> Error
    TypeMismatch "EIf_arms" (Prop -> Schema
    tMono Prop
    t1) (Prop -> Schema
    tMono Prop
    t2)

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

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

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

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

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

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

        ETAbs a :: TParam
    a e :: Expr
    e     ->
          do Forall as :: [TParam]
    as p :: [Prop]
    p t :: Prop
    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 (m :: * -> *) a. Monad m => a -> m a
    return ([TParam] -> [Prop] -> Prop -> Schema
    Forall (TParam
    a TParam -> [TParam] -> [TParam]
    forall a. a -> [a] -> [a]
    : [TParam]
    as) [Prop]
    p Prop
    t)

        ETApp e :: Expr
    e t :: Prop
    t ->
          do Kind
    k <- Prop -> TcM Kind
    checkType Prop
    t
             Schema
    s <- Expr -> TcM Schema
    exprSchema Expr
    e
             case Schema
    s of
               Forall (a :: TParam
    a : as :: [TParam]
    as) ps :: [Prop]
    ps t1 :: Prop
    t1 ->
                 do let vs :: Set TVar
    vs = Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Prop
    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
    $ \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 = TVar -> Prop -> Subst
    singleSubst (TParam -> TVar
    tpVar TParam
    a) Prop
    t
                    Schema -> TcM Schema
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Schema -> TcM Schema) -> Schema -> TcM Schema
    forall a b. (a -> b) -> a -> b
    $ [TParam] -> [Prop] -> Prop -> Schema
    Forall [TParam]
    as (Subst -> [Prop] -> [Prop]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Prop]
    ps) (Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Prop
    t1)

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

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

             case Prop -> Prop
    tNoUser Prop
    t1 of
               TCon (TC TCFun) [ a :: Prop
    a, b :: Prop
    b ]
                  | Prop -> Prop -> Bool
    forall a. Same a => a -> a -> Bool
    same Prop
    a Prop
    t2 -> Schema -> TcM Schema
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> Schema
    tMono Prop
    b)
               tf :: Prop
    tf -> Error -> TcM Schema
    forall a. Error -> TcM a
    reportError (Prop -> Prop -> Error
    BadApplication Prop
    tf Prop
    t1)

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

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

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

        -- XXX: Check that defined things are distinct?
        EWhere e :: Expr
    e dgs :: [DeclGroup]
    dgs ->
          let go :: [DeclGroup] -> TcM Schema
    go []       = Expr -> TcM Schema
    exprSchema Expr
    e
              go (d :: DeclGroup
    d : ds :: [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

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

        TupleSel n :: Int
    n mb :: Maybe Int
    mb ->

          case Prop -> Prop
    tNoUser Prop
    t of
            TCon (TC (TCTuple sz :: Int
    sz)) ts :: [Prop]
    ts ->
              do case Maybe Int
    mb of
                   Just sz1 :: 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))
                   Nothing  -> () -> TcM ()
    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)
                 Prop -> TcM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop -> TcM Prop) -> Prop -> TcM Prop
    forall a b. (a -> b) -> a -> b
    $ [Prop]
    ts [Prop] -> Int -> Prop
    forall a. [a] -> Int -> a
    !! Int
    n

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

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

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

        RecordSel f :: Ident
    f mb :: Maybe [Ident]
    mb ->
          case Prop -> Prop
    tNoUser Prop
    t of
            TRec fs :: [(Ident, Prop)]
    fs ->

              do case Maybe [Ident]
    mb of
                   Nothing -> () -> TcM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                   Just fs1 :: [Ident]
    fs1 ->
                     do let ns :: [Ident]
    ns  = [Ident] -> [Ident]
    forall a. Ord a => [a] -> [a]
    sort (((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Prop)]
    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 -> [(Ident, Prop)] -> Maybe Prop
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Ident
    f [(Ident, Prop)]
    fs of
                   Nothing -> Error -> TcM Prop
    forall a. Error -> TcM a
    reportError (Error -> TcM Prop) -> Error -> TcM Prop
    forall a b. (a -> b) -> a -> b
    $ Ident -> [Ident] -> Error
    MissingField Ident
    f ([Ident] -> Error) -> [Ident] -> Error
    forall a b. (a -> b) -> a -> b
    $ ((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Prop)]
    fs
                   Just ft :: Prop
    ft -> Prop -> TcM Prop
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    ft

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

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

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

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

              do case Maybe Int
    mb of
                   Nothing  -> () -> TcM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                   Just len :: Int
    len ->
                     case Prop -> Prop
    tNoUser Prop
    n of
                       TCon (TC (TCNum m :: 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 (m :: * -> *) a. Monad m => a -> m a
    return ()
                       _ -> Error -> TcM ()
    forall a. Error -> TcM a
    reportError (Error -> TcM ()) -> Error -> TcM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> Prop -> Error
    UnexpectedSequenceShape Int
    len Prop
    n

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

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

    -- | Check if the one type is convertible to the other.
    convertible :: Type -> Type -> TcM ()
    convertible :: Prop -> Prop -> TcM ()
    convertible t1 :: Prop
    t1 t2 :: Prop
    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  = Prop -> TcM ()
    proofObligation (Prop
    t1 Prop -> Prop -> Prop
    =#= Prop
    t2)
      where
      k1 :: Kind
    k1 = Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Prop
    t1
      k2 :: Kind
    k2 = Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Prop
    t2

    convertible t1 :: Prop
    t1 t2 :: Prop
    t2 = Prop -> Prop -> TcM ()
    go Prop
    t1 Prop
    t2
      where
      go :: Prop -> Prop -> TcM ()
    go ty1 :: Prop
    ty1 ty2 :: Prop
    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 "convertible" (Prop -> Schema
    tMono Prop
    ty1) (Prop -> Schema
    tMono Prop
    ty2)
            other :: Prop
    other = Prop -> Prop
    tNoUser Prop
    ty2

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

        in case Prop
    ty1 of
             TUser _ _ s :: Prop
    s   -> Prop -> Prop -> TcM ()
    go Prop
    s Prop
    ty2

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

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

             TRec fs :: [(Ident, Prop)]
    fs ->
               case Prop
    other of
                 TRec gs :: [(Ident, Prop)]
    gs ->
                   do let order :: [(Ident, b)] -> [(Ident, b)]
    order = ((Ident, b) -> (Ident, b) -> Ordering)
    -> [(Ident, b)] -> [(Ident, b)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (Ident -> Ident -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Ident -> Ident -> Ordering)
    -> ((Ident, b) -> Ident) -> (Ident, b) -> (Ident, b) -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Ident, b) -> Ident
    forall a b. (a, b) -> a
    fst)
                          fs1 :: [(Ident, Prop)]
    fs1   = [(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    order [(Ident, Prop)]
    fs
                          gs1 :: [(Ident, Prop)]
    gs1   = [(Ident, Prop)] -> [(Ident, Prop)]
    forall b. [(Ident, b)] -> [(Ident, b)]
    order [(Ident, Prop)]
    gs
                      Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Prop)]
    fs1 [Ident] -> [Ident] -> Bool
    forall a. Eq a => a -> a -> Bool
    == ((Ident, Prop) -> Ident) -> [(Ident, Prop)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Ident
    forall a b. (a, b) -> a
    fst [(Ident, Prop)]
    gs1) TcM ()
    forall a. TcM a
    err
                      [Prop] -> [Prop] -> TcM ()
    goMany (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Prop
    forall a b. (a, b) -> b
    snd [(Ident, Prop)]
    fs1) (((Ident, Prop) -> Prop) -> [(Ident, Prop)] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, Prop) -> Prop
    forall a b. (a, b) -> b
    snd [(Ident, Prop)]
    gs1)
                 _ -> 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 checkSig :: Bool
    checkSig d :: Decl
    d =
      case Decl -> DeclDef
    dDefinition Decl
    d of

        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 (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> Name
    dName Decl
    d, Decl -> Schema
    dSignature Decl
    d)

        DExpr e :: 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
             Bool -> TcM () -> TcM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Schema -> Schema -> Bool
    forall a. Same a => a -> a -> Bool
    same Schema
    s Schema
    s1) (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
    $ String -> Schema -> Schema -> Error
    TypeMismatch "DExpr" Schema
    s Schema
    s1
             (Name, Schema) -> TcM (Name, Schema)
    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 dg :: DeclGroup
    dg =
      case DeclGroup
    dg of
        NonRecursive d :: Decl
    d -> do (Name, Schema)
    x <- Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    True Decl
    d
                             [(Name, Schema)] -> TcM [(Name, Schema)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Name, Schema)
    x]
        Recursive ds :: [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
    $ \d :: Decl
    d ->
                      do Schema -> TcM ()
    checkSchema (Decl -> Schema
    dSignature Decl
    d)
                         (Name, Schema) -> TcM (Name, Schema)
    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)
    mapM (Bool -> Decl -> TcM (Name, Schema)
    checkDecl Bool
    False) [Decl]
    ds

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

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

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

    checkArm :: [Match] -> TcM ([(Name, Schema)], Type)
    checkArm :: [Match] -> TcM ([(Name, Schema)], Prop)
    checkArm []   = Error -> TcM ([(Name, Schema)], Prop)
    forall a. Error -> TcM a
    reportError Error
    EmptyArm
    checkArm [m :: Match
    m]  = do (x :: (Name, Schema)
    x,l :: Prop
    l) <- Match -> TcM ((Name, Schema), Prop)
    checkMatch Match
    m
                       ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Name, Schema)
    x], Prop
    l)
    checkArm (m :: Match
    m : ms :: [Match]
    ms) =
      do (x :: (Name, Schema)
    x, l :: Prop
    l)   <- Match -> TcM ((Name, Schema), Prop)
    checkMatch Match
    m
         (xs :: [(Name, Schema)]
    xs, l1 :: Prop
    l1) <- [(Name, Schema)]
    -> TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
    forall a. [(Name, Schema)] -> TcM a -> TcM a
    withVars [(Name, Schema)
    x] (TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop))
    -> TcM ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
    forall a b. (a -> b) -> a -> b
    $ [Match] -> TcM ([(Name, Schema)], Prop)
    checkArm [Match]
    ms
         let newLen :: Prop
    newLen = Prop -> Prop -> Prop
    tMul Prop
    l Prop
    l1
         ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop))
    -> ([(Name, Schema)], Prop) -> TcM ([(Name, Schema)], Prop)
    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 (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, Prop
    newLen)
                     else ((Name, Schema)
    x (Name, Schema) -> [(Name, Schema)] -> [(Name, Schema)]
    forall a. a -> [a] -> [a]
    : [(Name, Schema)]
    xs, Prop
    newLen)

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

    data RO = RO
      { RO -> Map Int TParam
    roTVars   :: Map Int TParam
      , RO -> [Prop]
    roAsmps   :: [Prop]
      , 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 Error (StateT RW Id)) a)

    instance Functor TcM where
      fmap :: (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 :: a -> TcM a
    pure  = a -> TcM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: 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 :: a -> TcM a
    return a :: a
    a    = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM (a -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a)
      TcM m :: ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m >>= :: TcM a -> (a -> TcM b) -> TcM b
    >>= f :: a -> TcM b
    f = ReaderT RO (ExceptionT Error (StateT RW Id)) b -> TcM b
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM (do a
    a <- ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m
                            let TcM m1 :: ReaderT RO (ExceptionT Error (StateT RW Id)) b
    m1 = a -> TcM b
    f a
    a
                            ReaderT RO (ExceptionT Error (StateT RW Id)) b
    m1)

    runTcM :: InferInput -> TcM a -> Either Error (a, [ProofObligation])
    runTcM :: InferInput -> TcM a -> Either Error (a, [Schema])
    runTcM env :: InferInput
    env (TcM m :: ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m) =
      case ReaderT RO (ExceptionT Error (StateT RW Id)) a
    -> RO -> RW -> (Either Error a, RW)
    forall (m :: * -> *) a r. RunM m a r => m a -> r
    runM ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m RO
    ro RW
    rw of
        (Left err :: Error
    err, _) -> Error -> Either Error (a, [Schema])
    forall a b. a -> Either a b
    Left Error
    err
        (Right a :: a
    a, s :: RW
    s)  -> (a, [Schema]) -> Either Error (a, [Schema])
    forall a b. b -> Either a b
    Right (a
    a, RW -> [Schema]
    woProofObligations RW
    s)
      where
      ro :: RO
    ro = RO :: Map Int TParam -> [Prop] -> Map Name Schema -> 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 (InferInput -> Map Name ModTParam
    inpParamTypes InferInput
    env)
                                          , let x :: TParam
    x = ModTParam -> TParam
    mtpParam ModTParam
    tp ]
              , roAsmps :: [Prop]
    roAsmps = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Prop -> Prop
    forall a. Located a -> a
    thing (InferInput -> [Located Prop]
    inpParamConstraints InferInput
    env)
              , 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModVParam -> Schema
    mvpType (InferInput -> Map Name ModVParam
    inpParamFuns InferInput
    env))
                            (InferInput -> Map Name Schema
    inpVars InferInput
    env)
              }
      rw :: RW
    rw = RW :: [Schema] -> 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 -> ShowS
    [Error] -> ShowS
    Error -> String
    (Int -> Error -> ShowS)
    -> (Error -> String) -> ([Error] -> ShowS) -> Show Error
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Error] -> ShowS
    $cshowList :: [Error] -> ShowS
    show :: Error -> String
    $cshow :: Error -> String
    showsPrec :: Int -> Error -> ShowS
    $cshowsPrec :: Int -> Error -> ShowS
    Show

    reportError :: Error -> TcM a
    reportError :: Error -> TcM a
    reportError e :: Error
    e = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM (Error -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise Error
    e)

    withTVar :: TParam -> TcM a -> TcM a
    withTVar :: TParam -> TcM a -> TcM a
    withTVar a :: TParam
    a (TcM m :: ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT Error (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
    -> ReaderT RO (ExceptionT 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 Error (StateT RW Id)) a
    m

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

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

    withVars :: [(Name, Schema)] -> TcM a -> TcM a
    withVars :: [(Name, Schema)] -> TcM a -> TcM a
    withVars xs :: [(Name, Schema)]
    xs (TcM m :: ReaderT RO (ExceptionT Error (StateT RW Id)) a
    m) = ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM (ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a)
    -> ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    forall a b. (a -> b) -> a -> b
    $
      do RO
    ro <- ReaderT RO (ExceptionT Error (StateT RW Id)) RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         RO
    -> ReaderT RO (ExceptionT Error (StateT RW Id)) a
    -> ReaderT RO (ExceptionT 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 Error (StateT RW Id)) a
    m

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

    lookupTVar :: TVar -> TcM Kind
    lookupTVar :: TVar -> TcM Kind
    lookupTVar x :: TVar
    x =
      case TVar
    x of
        TVFree {} -> Error -> TcM Kind
    forall a. Error -> TcM a
    reportError (TVar -> Error
    FreeTypeVariable TVar
    x)
        TVBound tpv :: 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 Error (StateT RW Id)) RO -> TcM RO
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM ReaderT RO (ExceptionT 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 tp :: 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 (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
                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 x :: Name
    x =
      do RO
    ro <- ReaderT RO (ExceptionT Error (StateT RW Id)) RO -> TcM RO
    forall a. ReaderT RO (ExceptionT Error (StateT RW Id)) a -> TcM a
    TcM ReaderT RO (ExceptionT 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 s :: Schema
    s -> Schema -> TcM Schema
    forall (m :: * -> *) a. Monad m => a -> m a
    return Schema
    s
           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