    -- |
    -- Module      :  Cryptol.TypeCheck.Solve
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
    module Cryptol.TypeCheck.Solve
      ( simplifyAllConstraints
      , proveImplication
      , tryProveImplication
      , proveModuleTopLevel
      , defaultAndSimplify
      , defaultReplExpr
      ) where

    import           Cryptol.Parser.Position(thing,emptyRange)
    import           Cryptol.TypeCheck.PP -- (pp)
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.Monad
    import           Cryptol.TypeCheck.Default
    import           Cryptol.TypeCheck.SimpType(tWidth)
    import           Cryptol.TypeCheck.Error(Error(..),Warning(..))
    import           Cryptol.TypeCheck.Subst
                        (apSubst, isEmptySubst, substToList,
                              emptySubst,Subst,(@@), Subst, listParamSubst)
    import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
    import           Cryptol.TypeCheck.Solver.Types
    import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)

    import           Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,isNumeric)
    import           Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
    import           Cryptol.TypeCheck.Solver.Numeric.Interval
    import           Cryptol.Utils.Patterns(matchMaybe)

    import           Control.Applicative ((<|>))
    import           Control.Monad(mzero)
    import           Data.Containers.ListUtils (nubOrd)
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import           Data.Set ( Set )
    import qualified Data.Set as Set
    import           Data.List(partition)
    import           Data.Maybe(listToMaybe,fromMaybe)

    quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst,[Goal]))
    quickSolverIO :: Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
    quickSolverIO Ctxt
    _ [] = Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    emptySubst, []))
    quickSolverIO Ctxt
    ctxt [Goal]
    gs =
      case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
    quickSolver Ctxt
    ctxt [Goal]
    gs of
        Left Error
    err -> Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Error -> Either Error (Subst, [Goal])
    forall a b. a -> Either a b
    Left Error
    err)
        Right (Subst
    su,[Goal]
    gs') ->
          do Doc -> IO ()
    forall {m :: * -> *} {p}. Monad m => p -> m ()
    msg ([Doc] -> Doc
    vcat ((Goal -> Doc) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type -> Doc
    forall a. PP a => a -> Doc
    pp (Type -> Doc) -> (Goal -> Type) -> Goal -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Type
    goal) [Goal]
    gs' [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Subst -> Doc
    forall a. PP a => a -> Doc
    pp Subst
    su]))
             Either Error (Subst, [Goal]) -> IO (Either Error (Subst, [Goal]))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[Goal]
    gs'))
      where
      msg :: p -> m ()
    msg p
    _ = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    {-
      shAsmps = case [ pp x <+> text "in" <+> ppInterval i |
                   (x,i) <- Map.toList ctxt ] of
                  [] -> text ""
                  xs -> text "ASMPS:" $$ nest 2 (vcat xs $$ text "===")
      msg d = putStrLn $ show (
                 text "quickSolver:" $$ nest 2 (vcat
                    [ shAsmps
                    , vcat (map (pp.goal) gs)
                    , text "==>"
                    , d
                    ])) -- -}

    quickSolver :: Ctxt   -- ^ Facts we can know
                -> [Goal] -- ^ Need to solve these
                -> Either Error (Subst,[Goal])
                -- ^ Left: contradicting goals,
                --   Right: inferred types, unsolved goals.
    quickSolver :: Ctxt -> [Goal] -> Either Error (Subst, [Goal])
    quickSolver Ctxt
    ctxt [Goal]
    gs0 = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go Subst
    emptySubst [] [Goal]
    gs0
      where
      go :: Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go Subst
    su [] [] = (Subst, [Goal]) -> Either Error (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[])

      go Subst
    su [Goal]
    unsolved [] =
        case Match (Either Error (Subst, [Goal]))
    -> Maybe (Either Error (Subst, [Goal]))
    forall a. Match a -> Maybe a
    matchMaybe (Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
    findImprovement Incompatible
    noIncompatible [Goal]
    unsolved) of
          Maybe (Either Error (Subst, [Goal]))
    Nothing -> (Subst, [Goal]) -> Either Error (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[Goal]
    unsolved)
          Just Either Error (Subst, [Goal])
    imp ->
            case Either Error (Subst, [Goal])
    imp of
              Right (Subst
    newSu, [Goal]
    subs) ->
                Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go (Subst
    newSu Subst -> Subst -> Subst
    @@ Subst
    su) [] ([Goal]
    subs [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++ Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    newSu [Goal]
    unsolved)
              Left Error
    err -> Error -> Either Error (Subst, [Goal])
    forall a b. a -> Either a b
    Left Error
    err

      go Subst
    su [Goal]
    unsolved (Goal
    g : [Goal]
    gs)
        | Type -> Set Type -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member (Goal -> Type
    goal Goal
    g) (Ctxt -> Set Type
    saturatedAsmps Ctxt
    ctxt) = Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go Subst
    su [Goal]
    unsolved [Goal]
    gs

      go Subst
    su [Goal]
    unsolved (Goal
    g : [Goal]
    gs) =
        case Ctxt -> Type -> Solved
    Simplify.simplifyStep Ctxt
    ctxt (Goal -> Type
    goal Goal
    g) of
          Solved
    Unsolvable          -> Error -> Either Error (Subst, [Goal])
    forall a b. a -> Either a b
    Left ([Goal] -> Error
    UnsolvableGoals [Goal
    g])
          Solved
    Unsolved            -> Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go Subst
    su (Goal
    g Goal -> [Goal] -> [Goal]
    forall a. a -> [a] -> [a]
    : [Goal]
    unsolved) [Goal]
    gs
          SolvedIf [Type]
    subs       ->
            let cvt :: Type -> Goal
    cvt Type
    x = Goal
    g { goal :: Type
    goal = Type
    x }
            in Subst -> [Goal] -> [Goal] -> Either Error (Subst, [Goal])
    go Subst
    su [Goal]
    unsolved ((Type -> Goal) -> [Type] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Goal
    cvt [Type]
    subs [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++ [Goal]
    gs)

      -- Probably better to find more than one.
      findImprovement :: Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
    findImprovement Incompatible
    inc [] =
        do let bad :: Map TVar (Goal, Goal)
    bad = (Goal -> Goal -> (Goal, Goal))
    -> Map TVar Goal -> Map TVar Goal -> Map TVar (Goal, Goal)
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    Map.intersectionWith (,) (Incompatible -> Map TVar Goal
    integralTVars Incompatible
    inc) (Incompatible -> Map TVar Goal
    fracTVars Incompatible
    inc)
           case Map TVar (Goal, Goal)
    -> Maybe ((Goal, Goal), Map TVar (Goal, Goal))
    forall k a. Map k a -> Maybe (a, Map k a)
    Map.minView Map TVar (Goal, Goal)
    bad of
             Just ((Goal
    g1,Goal
    g2),Map TVar (Goal, Goal)
    _) -> Either Error (Subst, [Goal])
    -> Match (Either Error (Subst, [Goal]))
    forall a. a -> Match a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either Error (Subst, [Goal])
     -> Match (Either Error (Subst, [Goal])))
    -> Either Error (Subst, [Goal])
    -> Match (Either Error (Subst, [Goal]))
    forall a b. (a -> b) -> a -> b
    $ Error -> Either Error (Subst, [Goal])
    forall a b. a -> Either a b
    Left (Error -> Either Error (Subst, [Goal]))
    -> Error -> Either Error (Subst, [Goal])
    forall a b. (a -> b) -> a -> b
    $ [Goal] -> Error
    UnsolvableGoals [Goal
    g1,Goal
    g2]
             Maybe ((Goal, Goal), Map TVar (Goal, Goal))
    Nothing -> Match (Either Error (Subst, [Goal]))
    forall a. Match a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

      findImprovement Incompatible
    inc (Goal
    g : [Goal]
    gs) =
        do (Subst
    su,[Type]
    ps) <- Bool -> Ctxt -> Type -> Match (Subst, [Type])
    improveProp Bool
    False Ctxt
    ctxt (Goal -> Type
    goal Goal
    g)
           Either Error (Subst, [Goal])
    -> Match (Either Error (Subst, [Goal]))
    forall a. a -> Match a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Subst, [Goal]) -> Either Error (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su, [ Goal
    g { goal :: Type
    goal = Type
    p } | Type
    p <- [Type]
    ps ]))
        Match (Either Error (Subst, [Goal]))
    -> Match (Either Error (Subst, [Goal]))
    -> Match (Either Error (Subst, [Goal]))
    forall a. Match a -> Match a -> Match a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
        Incompatible -> [Goal] -> Match (Either Error (Subst, [Goal]))
    findImprovement (Goal -> Incompatible -> Incompatible
    addIncompatible Goal
    g Incompatible
    inc) [Goal]
    gs

    --------------------------------------------------------------------------------
    -- Look for type variable with incompatible constraints

    data Incompatible = Incompatible
      { Incompatible -> Map TVar Goal
    integralTVars :: Map TVar Goal    -- ^ Integral a
      , Incompatible -> Map TVar Goal
    fracTVars     :: Map TVar Goal    -- ^ Field a or FLiteral
      }

    noIncompatible :: Incompatible
    noIncompatible :: Incompatible
    noIncompatible = Incompatible
      { integralTVars :: Map TVar Goal
    integralTVars = Map TVar Goal
    forall k a. Map k a
    Map.empty
      , fracTVars :: Map TVar Goal
    fracTVars     = Map TVar Goal
    forall k a. Map k a
    Map.empty
      }

    addIncompatible :: Goal -> Incompatible -> Incompatible
    addIncompatible :: Goal -> Incompatible -> Incompatible
    addIncompatible Goal
    g Incompatible
    i =
      Incompatible -> Maybe Incompatible -> Incompatible
    forall a. a -> Maybe a -> a
    fromMaybe Incompatible
    i (Maybe Incompatible -> Incompatible)
    -> Maybe Incompatible -> Incompatible
    forall a b. (a -> b) -> a -> b
    $
      do TVar
    tv <- Type -> Maybe TVar
    tIsVar (Type -> Maybe TVar) -> Maybe Type -> Maybe TVar
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> Maybe Type
    pIsIntegral (Goal -> Type
    goal Goal
    g)
         Incompatible -> Maybe Incompatible
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Incompatible
    i { integralTVars :: Map TVar Goal
    integralTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TVar
    tv Goal
    g (Incompatible -> Map TVar Goal
    integralTVars Incompatible
    i) }
      Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
      do TVar
    tv <- Type -> Maybe TVar
    tIsVar (Type -> Maybe TVar) -> Maybe Type -> Maybe TVar
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> Maybe Type
    pIsField (Goal -> Type
    goal Goal
    g)
         Incompatible -> Maybe Incompatible
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Incompatible
    i { fracTVars :: Map TVar Goal
    fracTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TVar
    tv Goal
    g (Incompatible -> Map TVar Goal
    fracTVars Incompatible
    i) }
      Maybe Incompatible -> Maybe Incompatible -> Maybe Incompatible
    forall a. Maybe a -> Maybe a -> Maybe a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
      do (Type
    _,Type
    _,Type
    _,Type
    t) <- Type -> Maybe (Type, Type, Type, Type)
    pIsFLiteral (Goal -> Type
    goal Goal
    g)
         TVar
    tv        <- Type -> Maybe TVar
    tIsVar Type
    t
         Incompatible -> Maybe Incompatible
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Incompatible
    i { fracTVars :: Map TVar Goal
    fracTVars = TVar -> Goal -> Map TVar Goal -> Map TVar Goal
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TVar
    tv Goal
    g (Incompatible -> Map TVar Goal
    fracTVars Incompatible
    i) }

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

    defaultReplExpr :: Solver -> Expr -> Schema ->
                        IO (Maybe ([(TParam,Type)], Expr))

    defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
    defaultReplExpr Solver
    sol Expr
    expr Schema
    sch =
      do Maybe [(TParam, Type)]
    mb <- Solver -> [TParam] -> [Type] -> IO (Maybe [(TParam, Type)])
    defaultReplExpr' Solver
    sol [TParam]
    numVs [Type]
    numPs
         case Maybe [(TParam, Type)]
    mb of
           Maybe [(TParam, Type)]
    Nothing -> Maybe ([(TParam, Type)], Expr)
    -> IO (Maybe ([(TParam, Type)], Expr))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([(TParam, Type)], Expr)
    forall a. Maybe a
    Nothing
           Just [(TParam, Type)]
    numBinds -> Maybe ([(TParam, Type)], Expr)
    -> IO (Maybe ([(TParam, Type)], Expr))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ([(TParam, Type)], Expr)
     -> IO (Maybe ([(TParam, Type)], Expr)))
    -> Maybe ([(TParam, Type)], Expr)
    -> IO (Maybe ([(TParam, Type)], Expr))
    forall a b. (a -> b) -> a -> b
    $
             do let optss :: [[(TParam, Type)]]
    optss = (TParam -> [(TParam, Type)]) -> [TParam] -> [[(TParam, Type)]]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> [(TParam, Type)]
    tryDefVar [TParam]
    otherVs
                [(TParam, Type)]
    su    <- [[(TParam, Type)]] -> Maybe [(TParam, Type)]
    forall a. [a] -> Maybe a
    listToMaybe
                           [ [(TParam, Type)]
    binds | [(TParam, Type)]
    nonSu <- [[(TParam, Type)]] -> [[(TParam, Type)]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [[(TParam, Type)]]
    optss
                                   , let binds :: [(TParam, Type)]
    binds = [(TParam, Type)]
    nonSu [(TParam, Type)] -> [(TParam, Type)] -> [(TParam, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [(TParam, Type)]
    numBinds
                                   , [(TParam, Type)] -> Bool
    validate [(TParam, Type)]
    binds ]
                [Type]
    tys <- [Maybe Type] -> Maybe [Type]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [ TParam -> [(TParam, Type)] -> Maybe Type
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup TParam
    v [(TParam, Type)]
    su | TParam
    v <- Schema -> [TParam]
    sVars Schema
    sch ]
                ([(TParam, Type)], Expr) -> Maybe ([(TParam, Type)], Expr)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(TParam, Type)]
    su, [Type] -> Expr
    forall {t :: * -> *}. Foldable t => t Type -> Expr
    appExpr [Type]
    tys)

      where
      validate :: [(TParam, Type)] -> Bool
    validate [(TParam, Type)]
    binds =
        let su :: Subst
    su = [(TParam, Type)] -> Subst
    listParamSubst [(TParam, Type)]
    binds
        in [Type] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ((Type -> [Type]) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Type -> [Type]
    pSplitAnd (Subst -> [Type] -> [Type]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Schema -> [Type]
    sProps Schema
    sch)))

      ([TParam]
    numVs,[TParam]
    otherVs) = (TParam -> Bool) -> [TParam] -> ([TParam], [TParam])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition (Kind -> TParam -> Bool
    forall {t}. HasKind t => Kind -> t -> Bool
    kindIs Kind
    KNum) (Schema -> [TParam]
    sVars Schema
    sch)
      ([Type]
    numPs,[Type]
    otherPs) = (Type -> Bool) -> [Type] -> ([Type], [Type])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Type -> Bool
    isNumeric (Schema -> [Type]
    sProps Schema
    sch)

      kindIs :: Kind -> t -> Bool
    kindIs Kind
    k t
    x = t -> Kind
    forall t. HasKind t => t -> Kind
    kindOf t
    x Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k

      gSet :: Goals
    gSet  = [Goal] -> Goals
    goalsFromList
               [ Goal { goal :: Type
    goal = Type
    p
                      , goalRange :: Range
    goalRange = Range
    emptyRange
                      , goalSource :: ConstraintSource
    goalSource = ConstraintSource
    CtDefaulting } | Type
    p <- [Type]
    otherPs ]

      fLitGoals :: Map TVar (Maybe ((TVar, Type), Warning))
    fLitGoals = Goals -> Map TVar (Maybe ((TVar, Type), Warning))
    flitDefaultCandidates Goals
    gSet

      tryDefVar :: TParam -> [(TParam, Type)]
      tryDefVar :: TParam -> [(TParam, Type)]
    tryDefVar TParam
    a
        -- REPL defaulting for floating-point literals
        | Just Maybe ((TVar, Type), Warning)
    m <- TVar
    -> Map TVar (Maybe ((TVar, Type), Warning))
    -> Maybe (Maybe ((TVar, Type), Warning))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (TParam -> TVar
    TVBound TParam
    a) Map TVar (Maybe ((TVar, Type), Warning))
    fLitGoals
        = case Maybe ((TVar, Type), Warning)
    m of
            Just ((TVar
    _,Type
    t),Warning
    _) -> [(TParam
    a,Type
    t)]
            Maybe ((TVar, Type), Warning)
    Nothing        -> []

        -- REPL defaulting for integer literals
        | Just Goal
    gt <- TVar -> Map TVar Goal -> Maybe Goal
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (TParam -> TVar
    TVBound TParam
    a) (Goals -> Map TVar Goal
    literalGoals Goals
    gSet)
        = let ok :: t -> Bool
    ok t
    p = Bool -> Bool
    not (TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member (TParam -> TVar
    TVBound TParam
    a) (t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs t
    p)) in
          [ (TParam
    a,Type
    t) | Type
    t <- [ Type
    tInteger, Type -> Type
    tWord (Type -> Type
    tWidth (Goal -> Type
    goal Goal
    gt)) ]
                  , Type -> Bool
    forall {t}. FVS t => t -> Bool
    ok Type
    t ]

        -- REPL defaulting for variables unconstrained by a literal constraint
        | Bool
    otherwise = [ (TParam
    a,Type
    t) | Type
    t <- [Type
    tInteger, Type
    tRational, Type
    tBit] ]

      appExpr :: t Type -> Expr
    appExpr t Type
    tys = (Expr -> Type -> Expr) -> Expr -> [Type] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\Expr
    e1 Type
    _ -> Expr -> Expr
    EProofApp Expr
    e1)
                          ((Expr -> Type -> Expr) -> Expr -> t Type -> Expr
    forall b a. (b -> a -> b) -> b -> t a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Expr -> Type -> Expr
    ETApp Expr
    expr t Type
    tys)
                          (Schema -> [Type]
    sProps Schema
    sch)

    defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning],[Error])
    defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
    defaultAndSimplify [TVar]
    as [Goal]
    gs =
      let ([TVar]
    as1, [Goal]
    gs1, Subst
    su1, [Warning]
    ws) = ([TVar], [Goal], Subst, [Warning])
    defLit
          ([TVar]
    as2, [Goal]
    gs2, Subst
    su2, [Error]
    errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    improveByDefaultingWithPure [TVar]
    as1 [Goal]
    gs1
      in ([TVar]
    as2,[Goal]
    gs2,Subst
    su2 Subst -> Subst -> Subst
    @@ Subst
    su1, [Warning]
    ws, [Error]
    errs)

      where
      defLit :: ([TVar], [Goal], Subst, [Warning])
    defLit
        | Subst -> Bool
    isEmptySubst Subst
    su = ([TVar], [Goal], Subst, [Warning])
    forall {a}. ([TVar], [Goal], Subst, [a])
    nope
        | Bool
    otherwise       = case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
    quickSolver Ctxt
    forall a. Monoid a => a
    mempty (Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    gs) of
                              Left Error
    _ -> ([TVar], [Goal], Subst, [Warning])
    forall {a}. ([TVar], [Goal], Subst, [a])
    nope -- hm?
                              Right (Subst
    su1,[Goal]
    gs1) -> ([TVar]
    as1,[Goal]
    gs1,Subst
    su1Subst -> Subst -> Subst
    @@Subst
    su,[Warning]
    ws)
        where ([TVar]
    as1,Subst
    su,[Warning]
    ws) = [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
    defaultLiterals [TVar]
    as [Goal]
    gs
              nope :: ([TVar], [Goal], Subst, [a])
    nope        = ([TVar]
    as,[Goal]
    gs,Subst
    emptySubst,[])

    simplifyAllConstraints :: InferM ()
    simplifyAllConstraints :: InferM ()
    simplifyAllConstraints =
      do InferM ()
    simpHasGoals
         [Goal]
    gs <- InferM [Goal]
    getGoals
         case [Goal]
    gs of
           [] -> () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
           [Goal]
    _ ->
            case Ctxt -> [Goal] -> Either Error (Subst, [Goal])
    quickSolver Ctxt
    forall a. Monoid a => a
    mempty [Goal]
    gs of
              Left Error
    err -> Error -> InferM ()
    recordError Error
    err
              Right (Subst
    su,[Goal]
    gs1) ->
                do Subst -> InferM ()
    extendSubst Subst
    su
                   [Goal] -> InferM ()
    addGoals [Goal]
    gs1

    -- | Simplify @Has@ constraints as much as possible.
    simpHasGoals :: InferM ()
    simpHasGoals :: InferM ()
    simpHasGoals = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
    go Bool
    False [] ([HasGoal] -> InferM ()) -> InferM [HasGoal] -> InferM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< InferM [HasGoal]
    getHasGoals
      where
      go :: Bool -> [HasGoal] -> [HasGoal] -> InferM ()
    go Bool
    _     []       []  = () -> InferM ()
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      go Bool
    True  [HasGoal]
    unsolved []  = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
    go Bool
    False [] [HasGoal]
    unsolved
      go Bool
    False [HasGoal]
    unsolved []  = (HasGoal -> InferM ()) -> [HasGoal] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ HasGoal -> InferM ()
    addHasGoal [HasGoal]
    unsolved

      go Bool
    changes [HasGoal]
    unsolved (HasGoal
    g : [HasGoal]
    todo) =
        do (Bool
    ch,Bool
    solved) <- HasGoal -> InferM (Bool, Bool)
    tryHasGoal HasGoal
    g
           let changes' :: Bool
    changes'  = Bool
    ch Bool -> Bool -> Bool
    || Bool
    changes
               unsolved' :: [HasGoal]
    unsolved' = if Bool
    solved then [HasGoal]
    unsolved else HasGoal
    g HasGoal -> [HasGoal] -> [HasGoal]
    forall a. a -> [a] -> [a]
    : [HasGoal]
    unsolved
           Bool
    changes' Bool -> InferM () -> InferM ()
    forall a b. a -> b -> b
    `seq` [HasGoal]
    unsolved [HasGoal] -> InferM () -> InferM ()
    forall a b. a -> b -> b
    `seq` Bool -> [HasGoal] -> [HasGoal] -> InferM ()
    go Bool
    changes' [HasGoal]
    unsolved' [HasGoal]
    todo

    -- | Try to clean-up any left-over constraints after we've checked everything
    -- in a module.  Typically these are either trivial things, or constraints
    -- on the module's type parameters.
    proveModuleTopLevel :: InferM ()
    proveModuleTopLevel :: InferM ()
    proveModuleTopLevel =
      do InferM ()
    simplifyAllConstraints
         [Goal]
    gs <- InferM [Goal]
    getGoals
         let vs :: [TVar]
    vs = Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList ((TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV ([Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    gs))
             ([TVar]
    _,[Goal]
    gs1,Subst
    su1,[Warning]
    ws,[Error]
    errs) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
    defaultAndSimplify [TVar]
    vs [Goal]
    gs
         Subst -> InferM ()
    extendSubst Subst
    su1
         (Warning -> InferM ()) -> [Warning] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Warning -> InferM ()
    recordWarning [Warning]
    ws
         (Error -> InferM ()) -> [Error] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Error -> InferM ()
    recordError [Error]
    errs

         [Located Type]
    cs <- InferM [Located Type]
    getParamConstraints
         case [Located Type]
    cs of
           [] -> [Goal] -> InferM ()
    addGoals [Goal]
    gs1
           [Located Type]
    _  -> do Subst
    su2 <- Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
    proveImplication Bool
    False Maybe Name
    forall a. Maybe a
    Nothing [] [] [Goal]
    gs1
                    Subst -> InferM ()
    extendSubst Subst
    su2

    -- | Prove an implication, and return any improvements that we computed.
    -- Records errors, if any of the goals couldn't be solved.
    proveImplication :: Bool -> Maybe Name ->
      [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication :: Bool -> Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Subst
    proveImplication Bool
    dedupErrs Maybe Name
    lnam [TParam]
    as [Type]
    ps [Goal]
    gs =
      do Set TVar
    evars <- InferM (Set TVar)
    varsWithAsmps
         Solver
    solver <- InferM Solver
    getSolver

         [TParam]
    extraAs <- ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam ([ModTParam] -> [TParam])
    -> (Map Name ModTParam -> [ModTParam])
    -> Map Name ModTParam
    -> [TParam]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems) (Map Name ModTParam -> [TParam])
    -> InferM (Map Name ModTParam) -> InferM [TParam]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name ModTParam)
    getParamTypes
         [Type]
    extra   <- (Located Type -> Type) -> [Located Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Type -> Type
    forall a. Located a -> a
    thing ([Located Type] -> [Type])
    -> InferM [Located Type] -> InferM [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM [Located Type]
    getParamConstraints

         (Either [Error] [Warning]
    mbErr,Subst
    su) <- IO (Either [Error] [Warning], Subst)
    -> InferM (Either [Error] [Warning], Subst)
    forall a. IO a -> InferM a
    io (Solver
    -> Bool
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Type]
    -> [Goal]
    -> IO (Either [Error] [Warning], Subst)
    proveImplicationIO Solver
    solver Bool
    dedupErrs Maybe Name
    lnam Set TVar
    evars
                                ([TParam]
    extraAs [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ [TParam]
    as) ([Type]
    extra [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ [Type]
    ps) [Goal]
    gs)
         case Either [Error] [Warning]
    mbErr of
           Right [Warning]
    ws  -> (Warning -> InferM ()) -> [Warning] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Warning -> InferM ()
    recordWarning [Warning]
    ws
           Left [Error]
    errs -> (Error -> InferM ()) -> [Error] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Error -> InferM ()
    recordError [Error]
    errs
         Subst -> InferM Subst
    forall a. a -> InferM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Subst
    su

    -- | Tries to prove an implication. If proved, then returns `Right (m_su ::
    -- InferM Subst)` where `m_su` is an `InferM` computation that results in the
    -- solution substitution, and records any warning invoked during proving. If not
    -- proved, then returns `Left (m_err :: InferM ())`, which records all errors
    -- invoked during proving.
    tryProveImplication ::
      Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
    tryProveImplication :: Maybe Name -> [TParam] -> [Type] -> [Goal] -> InferM Bool
    tryProveImplication Maybe Name
    lnam [TParam]
    as [Type]
    ps [Goal]
    gs =
      do Set TVar
    evars <- InferM (Set TVar)
    varsWithAsmps
         Solver
    solver <- InferM Solver
    getSolver

         [TParam]
    extraAs <- ((ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    mtpParam ([ModTParam] -> [TParam])
    -> (Map Name ModTParam -> [ModTParam])
    -> Map Name ModTParam
    -> [TParam]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems) (Map Name ModTParam -> [TParam])
    -> InferM (Map Name ModTParam) -> InferM [TParam]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM (Map Name ModTParam)
    getParamTypes
         [Type]
    extra   <- (Located Type -> Type) -> [Located Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Type -> Type
    forall a. Located a -> a
    thing ([Located Type] -> [Type])
    -> InferM [Located Type] -> InferM [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM [Located Type]
    getParamConstraints

         (Either [Error] [Warning]
    mbErr,Subst
    _su) <- IO (Either [Error] [Warning], Subst)
    -> InferM (Either [Error] [Warning], Subst)
    forall a. IO a -> InferM a
    io (Solver
    -> Bool
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Type]
    -> [Goal]
    -> IO (Either [Error] [Warning], Subst)
    proveImplicationIO Solver
    solver Bool
    False Maybe Name
    lnam Set TVar
    evars
                                ([TParam]
    extraAs [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ [TParam]
    as) ([Type]
    extra [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ [Type]
    ps) [Goal]
    gs)
         case Either [Error] [Warning]
    mbErr of
           Left {}  -> Bool -> InferM Bool
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
           Right {} -> Bool -> InferM Bool
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True

    proveImplicationIO :: Solver
                       -> Bool     -- ^ Whether to remove duplicate goals in errors
                       -> Maybe Name     -- ^ Checking this function
                       -> Set TVar -- ^ These appear in the env., and we should
                                   -- not try to default them
                       -> [TParam] -- ^ Type parameters
                       -> [Prop]   -- ^ Assumed constraint
                       -> [Goal]   -- ^ Collected constraints
                       -> IO (Either [Error] [Warning], Subst)
    proveImplicationIO :: Solver
    -> Bool
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Type]
    -> [Goal]
    -> IO (Either [Error] [Warning], Subst)
    proveImplicationIO Solver
    _ Bool
    _         Maybe Name
    _ Set TVar
    _         [TParam]
    _  []     []  = (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either [Error] [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    emptySubst)
    proveImplicationIO Solver
    s Bool
    dedupErrs Maybe Name
    f Set TVar
    varsInEnv [TParam]
    ps [Type]
    asmps0 [Goal]
    gs0 =
      do let ctxt :: Ctxt
    ctxt = [Type] -> Ctxt
    buildSolverCtxt [Type]
    asmps
         Either Error (Subst, [Goal])
    res <- Ctxt -> [Goal] -> IO (Either Error (Subst, [Goal]))
    quickSolverIO Ctxt
    ctxt [Goal]
    gs
         case Either Error (Subst, [Goal])
    res of
           Left Error
    erro -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Error] -> Either [Error] [Warning]
    forall a b. a -> Either a b
    Left [Error
    erro], Subst
    emptySubst)
           Right (Subst
    su,[]) -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either [Error] [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    su)
           Right (Subst
    su,[Goal]
    gs1) ->
             do [Goal]
    gs2 <- Solver -> [Type] -> [Goal] -> IO [Goal]
    proveImp Solver
    s [Type]
    asmps [Goal]
    gs1
                case [Goal]
    gs2 of
                  [] -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either [Error] [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    su)
                  [Goal]
    gs3 ->
                    do let free :: [TVar]
    free = (TVar -> Bool) -> [TVar] -> [TVar]
    forall a. (a -> Bool) -> [a] -> [a]
    filter TVar -> Bool
    isFreeTV
                                ([TVar] -> [TVar]) -> [TVar] -> [TVar]
    forall a b. (a -> b) -> a -> b
    $ Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList
                                (Set TVar -> [TVar]) -> Set TVar -> [TVar]
    forall a b. (a -> b) -> a -> b
    $ Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    Set.difference ([Type] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs ((Goal -> Type) -> [Goal] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Type
    goal [Goal]
    gs3)) Set TVar
    varsInEnv
                       case [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
    defaultAndSimplify [TVar]
    free [Goal]
    gs3 of
                         ([TVar]
    _,[Goal]
    _,Subst
    newSu,[Warning]
    _,[Error]
    errs)
                            | Subst -> Bool
    isEmptySubst Subst
    newSu ->
                                     (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Error] -> Either [Error] [Warning]
    forall a b. a -> Either a b
    Left ([Goal] -> Error
    err [Goal]
    gs3Error -> [Error] -> [Error]
    forall a. a -> [a] -> [a]
    :[Error]
    errs), Subst
    su) -- XXX: Old?
                         ([TVar]
    _,[Goal]
    newGs,Subst
    newSu,[Warning]
    ws,[Error]
    errs) ->
                           do let su1 :: Subst
    su1 = Subst
    newSu Subst -> Subst -> Subst
    @@ Subst
    su
                              (Either [Error] [Warning]
    res1,Subst
    su2) <- Solver
    -> Bool
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Type]
    -> [Goal]
    -> IO (Either [Error] [Warning], Subst)
    proveImplicationIO Solver
    s Bool
    dedupErrs Maybe Name
    f Set TVar
    varsInEnv [TParam]
    ps
                                                     (Subst -> [Type] -> [Type]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 [Type]
    asmps0) [Goal]
    newGs
                              let su3 :: Subst
    su3 = Subst
    su2 Subst -> Subst -> Subst
    @@ Subst
    su1
                              case Either [Error] [Warning]
    res1 of
                                Left [Error]
    bad -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Error] -> Either [Error] [Warning]
    forall a b. a -> Either a b
    Left ([Error]
    bad [Error] -> [Error] -> [Error]
    forall a. [a] -> [a] -> [a]
    ++ [Error]
    errs), Subst
    su3)
                                Right [Warning]
    ws1
                                  | [Error] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Error]
    errs -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either [Error] [Warning]
    forall a b. b -> Either a b
    Right ([Warning]
    ws[Warning] -> [Warning] -> [Warning]
    forall a. [a] -> [a] -> [a]
    ++[Warning]
    ws1),Subst
    su3)
                                  | Bool
    otherwise -> (Either [Error] [Warning], Subst)
    -> IO (Either [Error] [Warning], Subst)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Error] -> Either [Error] [Warning]
    forall a b. a -> Either a b
    Left [Error]
    errs, Subst
    su3)
      where
      err :: [Goal] -> Error
    err [Goal]
    us = Error -> Error
    cleanupError
               (Error -> Error) -> Error -> Error
    forall a b. (a -> b) -> a -> b
    $ DelayedCt -> Error
    UnsolvedDelayedCt
               (DelayedCt -> Error) -> DelayedCt -> Error
    forall a b. (a -> b) -> a -> b
    $ DelayedCt { dctSource :: Maybe Name
    dctSource = Maybe Name
    f
                           , dctForall :: [TParam]
    dctForall = [TParam]
    ps
                           , dctAsmps :: [Type]
    dctAsmps  = [Type]
    asmps0
                           , dctGoals :: [Goal]
    dctGoals  = if Bool
    dedupErrs then [Goal] -> [Goal]
    forall a. Ord a => [a] -> [a]
    nubOrd [Goal]
    us else [Goal]
    us
                           }

      asmps1 :: [Type]
    asmps1 = (Type -> [Type]) -> [Type] -> [Type]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Type -> [Type]
    pSplitAnd [Type]
    asmps0
      ([Type]
    asmps,[Goal]
    gs) =
         let gs1 :: [Goal]
    gs1 = [ Goal
    g { goal :: Type
    goal = Type
    p } | Goal
    g <- [Goal]
    gs0, Type
    p <- Type -> [Type]
    pSplitAnd (Goal -> Type
    goal Goal
    g)
                                    , Type -> [Type] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    notElem Type
    p [Type]
    asmps1 ]
         in case Match (Subst, [Type]) -> Maybe (Subst, [Type])
    forall a. Match a -> Maybe a
    matchMaybe (Bool -> Ctxt -> [Type] -> Match (Subst, [Type])
    improveProps Bool
    True Ctxt
    forall a. Monoid a => a
    mempty [Type]
    asmps1) of
              Maybe (Subst, [Type])
    Nothing -> ([Type]
    asmps1,[Goal]
    gs1)
              Just (Subst
    newSu,[Type]
    newAsmps) ->
                 ( [ TVar -> Type
    TVar TVar
    x Type -> Type -> Type
    =#= Type
    t | (TVar
    x,Type
    t) <- Subst -> [(TVar, Type)]
    substToList Subst
    newSu ]
                   [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ [Type]
    newAsmps
                 , [ Goal
    g { goal :: Type
    goal = Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    newSu (Goal -> Type
    goal Goal
    g) } | Goal
    g <- [Goal]
    gs1 ]
                 )

    cleanupError :: Error -> Error
    cleanupError :: Error -> Error
    cleanupError Error
    err =
      case Error
    err of
        UnsolvedDelayedCt DelayedCt
    d ->
          let noInferVars :: Goal -> Bool
    noInferVars = Set TVar -> Bool
    forall a. Set a -> Bool
    Set.null (Set TVar -> Bool) -> (Goal -> Set TVar) -> Goal -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TVar -> Bool) -> Set TVar -> Set TVar
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter TVar -> Bool
    isFreeTV (Set TVar -> Set TVar) -> (Goal -> Set TVar) -> Goal -> Set TVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Type -> Set TVar) -> (Goal -> Type) -> Goal -> Set TVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Type
    goal
              without :: [Goal]
    without = (Goal -> Bool) -> [Goal] -> [Goal]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Goal -> Bool
    noInferVars (DelayedCt -> [Goal]
    dctGoals DelayedCt
    d)
          in DelayedCt -> Error
    UnsolvedDelayedCt (DelayedCt -> Error) -> DelayedCt -> Error
    forall a b. (a -> b) -> a -> b
    $
                if Bool -> Bool
    not ([Goal] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Goal]
    without) then DelayedCt
    d { dctGoals :: [Goal]
    dctGoals = [Goal]
    without } else DelayedCt
    d

        Error
    _ -> Error
    err

    buildSolverCtxt :: [Prop] -> Ctxt
    buildSolverCtxt :: [Type] -> Ctxt
    buildSolverCtxt [Type]
    ps0 =
      let ps :: Set Type
    ps = Set Type -> [Type] -> Set Type
    saturateProps Set Type
    forall a. Monoid a => a
    mempty [Type]
    ps0
          ivals :: Map TVar Interval
    ivals = Map TVar Interval -> [Type] -> Map TVar Interval
    assumptionIntervals Map TVar Interval
    forall a. Monoid a => a
    mempty (Set Type -> [Type]
    forall a. Set a -> [a]
    Set.toList Set Type
    ps)
       in SolverCtxt
          { intervals :: Map TVar Interval
    intervals = Map TVar Interval
    ivals
          , saturatedAsmps :: Set Type
    saturatedAsmps = Set Type
    ps
          }

     where
     saturateProps :: Set Type -> [Type] -> Set Type
    saturateProps Set Type
    gs [] = Set Type
    gs
     saturateProps Set Type
    gs (Type
    p:[Type]
    ps)
       | Type -> Set Type -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Type
    p Set Type
    gs = Set Type -> [Type] -> Set Type
    saturateProps Set Type
    gs [Type]
    ps
       | Just (Type
    n,Type
    _) <- Type -> Maybe (Type, Type)
    pIsLiteral Type
    p =
           let gs' :: Set Type
    gs' = [Type] -> Set Type
    forall a. Ord a => [a] -> Set a
    Set.fromList [Type
    p, Type -> Type
    pFin Type
    n] Set Type -> Set Type -> Set Type
    forall a. Semigroup a => a -> a -> a
    <> Set Type
    gs
            in Set Type -> [Type] -> Set Type
    saturateProps Set Type
    gs' [Type]
    ps
       | Bool
    otherwise =
            let gs' :: Set Type
    gs' = Type -> Set Type
    forall a. a -> Set a
    Set.singleton Type
    p Set Type -> Set Type -> Set Type
    forall a. Semigroup a => a -> a -> a
    <> Type -> Set Type
    superclassSet Type
    p Set Type -> Set Type -> Set Type
    forall a. Semigroup a => a -> a -> a
    <> Set Type
    gs
             in Set Type -> [Type] -> Set Type
    saturateProps Set Type
    gs' [Type]
    ps

     assumptionIntervals :: Map TVar Interval -> [Type] -> Map TVar Interval
    assumptionIntervals Map TVar Interval
    as [Type]
    ps =
       case Map TVar Interval -> [Type] -> IntervalUpdate
    computePropIntervals Map TVar Interval
    as [Type]
    ps of
         IntervalUpdate
    NoChange -> Map TVar Interval
    as
         InvalidInterval {} -> Map TVar Interval
    as -- XXX: say something
         NewIntervals Map TVar Interval
    bs -> Map TVar Interval -> Map TVar Interval -> Map TVar Interval
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map TVar Interval
    bs Map TVar Interval
    as