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

    {-# LANGUAGE PatternGuards, BangPatterns, RecordWildCards #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Solve
      ( simplifyAllConstraints
      , proveImplication
      , 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.PP (text,vcat,(<+>))
    import           Cryptol.Utils.Patterns(matchMaybe)

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

    quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst,[Goal]))
    quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst, [Goal]))
    quickSolverIO _ [] = Either Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Subst, [Goal]) -> Either Goal (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    emptySubst, []))
    quickSolverIO ctxt :: Ctxt
    ctxt gs :: [Goal]
    gs =
      case Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
    quickSolver Ctxt
    ctxt [Goal]
    gs of
        Left err :: Goal
    err ->
          do Doc -> IO ()
    forall (m :: * -> *) p. Monad m => p -> m ()
    msg (String -> Doc
    text "Contradiction:" Doc -> Doc -> Doc
    <+> Prop -> Doc
    forall a. PP a => a -> Doc
    pp (Goal -> Prop
    goal Goal
    err))
             Either Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Goal -> Either Goal (Subst, [Goal])
    forall a b. a -> Either a b
    Left Goal
    err)
        Right (su :: Subst
    su,gs' :: [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 (Prop -> Doc
    forall a. PP a => a -> Doc
    pp (Prop -> Doc) -> (Goal -> Prop) -> Goal -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Prop
    goal) [Goal]
    gs' [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Subst -> Doc
    forall a. PP a => a -> Doc
    pp Subst
    su]))
             Either Goal (Subst, [Goal]) -> IO (Either Goal (Subst, [Goal]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Subst, [Goal]) -> Either Goal (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[Goal]
    gs'))
      where
      msg :: p -> m ()
    msg _ = () -> m ()
    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 Goal (Subst,[Goal])
                -- ^ Left: contradicting goals,
                --   Right: inferred types, unsolved goals.
    quickSolver :: Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
    quickSolver ctxt :: Ctxt
    ctxt gs0 :: [Goal]
    gs0 = Subst -> [Goal] -> [Goal] -> Either Goal (Subst, [Goal])
    go Subst
    emptySubst [] [Goal]
    gs0
      where
      go :: Subst -> [Goal] -> [Goal] -> Either Goal (Subst, [Goal])
    go su :: Subst
    su [] [] = (Subst, [Goal]) -> Either Goal (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[])

      go su :: Subst
    su unsolved :: [Goal]
    unsolved [] =
        case Match (Subst, [Goal]) -> Maybe (Subst, [Goal])
    forall a. Match a -> Maybe a
    matchMaybe ([Goal] -> Match (Subst, [Goal])
    findImprovement [Goal]
    unsolved) of
          Nothing            -> (Subst, [Goal]) -> Either Goal (Subst, [Goal])
    forall a b. b -> Either a b
    Right (Subst
    su,[Goal]
    unsolved)
          Just (newSu :: Subst
    newSu, subs :: [Goal]
    subs) -> Subst -> [Goal] -> [Goal] -> Either Goal (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)

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

      -- Probably better to find more than one.
      findImprovement :: [Goal] -> Match (Subst, [Goal])
    findImprovement []       = Match (Subst, [Goal])
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      findImprovement (g :: Goal
    g : gs :: [Goal]
    gs) =
        do (su :: Subst
    su,ps :: [Prop]
    ps) <- Bool -> Ctxt -> Prop -> Match (Subst, [Prop])
    improveProp Bool
    False Ctxt
    ctxt (Goal -> Prop
    goal Goal
    g)
           (Subst, [Goal]) -> Match (Subst, [Goal])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Subst
    su, [ Goal
    g { goal :: Prop
    goal = Prop
    p } | Prop
    p <- [Prop]
    ps ])
        Match (Subst, [Goal])
    -> Match (Subst, [Goal]) -> Match (Subst, [Goal])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> [Goal] -> Match (Subst, [Goal])
    findImprovement [Goal]
    gs

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

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

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

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

      (numVs :: [TParam]
    numVs,otherVs :: [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)
      (numPs :: [Prop]
    numPs,otherPs :: [Prop]
    otherPs) = (Prop -> Bool) -> [Prop] -> ([Prop], [Prop])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Prop -> Bool
    isNumeric (Schema -> [Prop]
    sProps Schema
    sch)

      kindIs :: Kind -> t -> Bool
    kindIs k :: Kind
    k x :: 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 :: ConstraintSource -> Range -> Prop -> Goal
    Goal { goal :: Prop
    goal = Prop
    p
                      , goalRange :: Range
    goalRange = Range
    emptyRange
                      , goalSource :: ConstraintSource
    goalSource = ConstraintSource
    CtDefaulting } | Prop
    p <- [Prop]
    otherPs ]

      tryDefVar :: TParam -> Maybe [(TParam, Prop)]
    tryDefVar a :: TParam
    a =
        do let a' :: TVar
    a' = TParam -> TVar
    TVBound TParam
    a
           Goal
    gt <- TVar -> Map TVar Goal -> Maybe Goal
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TVar
    a' (Goals -> Map TVar Goal
    literalGoals Goals
    gSet)
           let ok :: t -> Bool
    ok p :: t
    p = Bool -> Bool
    not (TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member TVar
    a' (t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs t
    p))
           [(TParam, Prop)] -> Maybe [(TParam, Prop)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ (TParam
    a,Prop
    t) | Prop
    t <- [ Prop
    tInteger, Prop
    tBit, Prop -> Prop
    tWord (Prop -> Prop
    tWidth (Goal -> Prop
    goal Goal
    gt)) ]
                          , Prop -> Bool
    forall t. FVS t => t -> Bool
    ok Prop
    t ]

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

    defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar],[Goal],Subst,[Warning])
    defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    defaultAndSimplify as :: [TVar]
    as gs :: [Goal]
    gs =
      let (as1 :: [TVar]
    as1, gs1 :: [Goal]
    gs1, su1 :: Subst
    su1, ws1 :: [Warning]
    ws1) = ([TVar], [Goal], Subst, [Warning])
    defLit
          (as2 :: [TVar]
    as2, gs2 :: [Goal]
    gs2, su2 :: Subst
    su2, ws2 :: [Warning]
    ws2) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    improveByDefaultingWithPure [TVar]
    as1 [Goal]
    gs1
      in ([TVar]
    as2,[Goal]
    gs2,Subst
    su2 Subst -> Subst -> Subst
    @@ Subst
    su1, [Warning]
    ws1 [Warning] -> [Warning] -> [Warning]
    forall a. [a] -> [a] -> [a]
    ++ [Warning]
    ws2)
      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 Goal (Subst, [Goal])
    quickSolver Ctxt
    forall k a. Map k a
    Map.empty (Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    gs) of
                              Left _ -> ([TVar], [Goal], Subst, [Warning])
    forall a. ([TVar], [Goal], Subst, [a])
    nope -- hm?
                              Right (su1 :: Subst
    su1,gs1 :: [Goal]
    gs1) -> ([TVar]
    as1,[Goal]
    gs1,Subst
    su1Subst -> Subst -> Subst
    @@Subst
    su,[Warning]
    ws)
        where (as1 :: [TVar]
    as1,su :: Subst
    su,ws :: [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 (m :: * -> *) a. Monad m => a -> m a
    return ()
           _ ->
            case Ctxt -> [Goal] -> Either Goal (Subst, [Goal])
    quickSolver Ctxt
    forall k a. Map k a
    Map.empty [Goal]
    gs of
              Left badG :: Goal
    badG      -> Error -> InferM ()
    recordError (Bool -> [Goal] -> Error
    UnsolvedGoals Bool
    True [Goal
    badG])
              Right (su :: Subst
    su,gs1 :: [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 _     []       []  = () -> InferM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      go True  unsolved :: [HasGoal]
    unsolved []  = Bool -> [HasGoal] -> [HasGoal] -> InferM ()
    go Bool
    False [] [HasGoal]
    unsolved
      go False unsolved :: [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 changes :: Bool
    changes unsolved :: [HasGoal]
    unsolved (g :: HasGoal
    g : todo :: [HasGoal]
    todo) =
        do (ch :: Bool
    ch,solved :: 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))
             (_,gs1 :: [Goal]
    gs1,su1 :: Subst
    su1,ws :: [Warning]
    ws) = [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    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

         [Located Prop]
    cs <- InferM [Located Prop]
    getParamConstraints
         case [Located Prop]
    cs of
           [] -> [Goal] -> InferM ()
    addGoals [Goal]
    gs1
           _  -> do Subst
    su2 <- Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication 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 :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
    proveImplication lnam :: Maybe Name
    lnam as :: [TParam]
    as ps :: [Prop]
    ps gs :: [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
         [Prop]
    extra   <- (Located Prop -> Prop) -> [Located Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Prop -> Prop
    forall a. Located a -> a
    thing ([Located Prop] -> [Prop])
    -> InferM [Located Prop] -> InferM [Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InferM [Located Prop]
    getParamConstraints

         (mbErr :: Either Error [Warning]
    mbErr,su :: Subst
    su) <- IO (Either Error [Warning], Subst)
    -> InferM (Either Error [Warning], Subst)
    forall a. IO a -> InferM a
    io (Solver
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Prop]
    -> [Goal]
    -> IO (Either Error [Warning], Subst)
    proveImplicationIO Solver
    solver Maybe Name
    lnam Set TVar
    evars
                                ([TParam]
    extraAs [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ [TParam]
    as) ([Prop]
    extra [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ps) [Goal]
    gs)
         case Either Error [Warning]
    mbErr of
           Right ws :: [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 err :: Error
    err -> Error -> InferM ()
    recordError Error
    err
         Subst -> InferM Subst
    forall (m :: * -> *) a. Monad m => a -> m a
    return Subst
    su

    proveImplicationIO :: Solver
                       -> 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
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Prop]
    -> [Goal]
    -> IO (Either Error [Warning], Subst)
    proveImplicationIO _   _     _         _  [] [] = (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either Error [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    emptySubst)
    proveImplicationIO s :: Solver
    s f :: Maybe Name
    f varsInEnv :: Set TVar
    varsInEnv ps :: [TParam]
    ps asmps0 :: [Prop]
    asmps0 gs0 :: [Goal]
    gs0 =
      do let ctxt :: Ctxt
    ctxt = Ctxt -> [Prop] -> Ctxt
    assumptionIntervals Ctxt
    forall k a. Map k a
    Map.empty [Prop]
    asmps
         Either Goal (Subst, [Goal])
    res <- Ctxt -> [Goal] -> IO (Either Goal (Subst, [Goal]))
    quickSolverIO Ctxt
    ctxt [Goal]
    gs
         case Either Goal (Subst, [Goal])
    res of
           Left bad :: Goal
    bad -> (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Error -> Either Error [Warning]
    forall a b. a -> Either a b
    Left (Bool -> [Goal] -> Error
    UnsolvedGoals Bool
    True [Goal
    bad]), Subst
    emptySubst)
           Right (su :: Subst
    su,[]) -> (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either Error [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    su)
           Right (su :: Subst
    su,gs1 :: [Goal]
    gs1) ->
             do [Goal]
    gs2 <- Solver -> [Prop] -> [Goal] -> IO [Goal]
    proveImp Solver
    s [Prop]
    asmps [Goal]
    gs1
                case [Goal]
    gs2 of
                  [] -> (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Warning] -> Either Error [Warning]
    forall a b. b -> Either a b
    Right [], Subst
    su)
                  gs3 :: [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 ([Prop] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs ((Goal -> Prop) -> [Goal] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Prop
    goal [Goal]
    gs3)) Set TVar
    varsInEnv
                       case [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    defaultAndSimplify [TVar]
    free [Goal]
    gs3 of
                         (_,_,newSu :: Subst
    newSu,_)
                            | Subst -> Bool
    isEmptySubst Subst
    newSu ->
                                     (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Goal] -> Either Error [Warning]
    forall b. [Goal] -> Either Error b
    err [Goal]
    gs3, Subst
    su) -- XXX: Old?
                         (_,newGs :: [Goal]
    newGs,newSu :: Subst
    newSu,ws :: [Warning]
    ws) ->
                           do let su1 :: Subst
    su1 = Subst
    newSu Subst -> Subst -> Subst
    @@ Subst
    su
                              (res1 :: Either Error [Warning]
    res1,su2 :: Subst
    su2) <- Solver
    -> Maybe Name
    -> Set TVar
    -> [TParam]
    -> [Prop]
    -> [Goal]
    -> IO (Either Error [Warning], Subst)
    proveImplicationIO Solver
    s Maybe Name
    f Set TVar
    varsInEnv [TParam]
    ps
                                                     (Subst -> [Prop] -> [Prop]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 [Prop]
    asmps0) [Goal]
    newGs
                              let su3 :: Subst
    su3 = Subst
    su2 Subst -> Subst -> Subst
    @@ Subst
    su1
                              case Either Error [Warning]
    res1 of
                                Left bad :: Error
    bad -> (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Error -> Either Error [Warning]
    forall a b. a -> Either a b
    Left Error
    bad, Subst
    su3)
                                Right ws1 :: [Warning]
    ws1 -> (Either Error [Warning], Subst)
    -> IO (Either Error [Warning], Subst)
    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)
      where
      err :: [Goal] -> Either Error b
    err us :: [Goal]
    us =  Error -> Either Error b
    forall a b. a -> Either a b
    Left (Error -> Either Error b) -> Error -> Either Error b
    forall a b. (a -> b) -> a -> b
    $ 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 :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt
    DelayedCt { dctSource :: Maybe Name
    dctSource = Maybe Name
    f
                                 , dctForall :: [TParam]
    dctForall = [TParam]
    ps
                                 , dctAsmps :: [Prop]
    dctAsmps  = [Prop]
    asmps0
                                 , dctGoals :: [Goal]
    dctGoals  = [Goal]
    us
                                 }

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

    cleanupError :: Error -> Error
    cleanupError :: Error -> Error
    cleanupError err :: Error
    err =
      case Error
    err of
        UnsolvedDelayedCt d :: 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
    . Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Prop -> Set TVar) -> (Goal -> Prop) -> Goal -> Set TVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Goal -> Prop
    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 (t :: * -> *) a. Foldable t => t a -> Bool
    null [Goal]
    without) then DelayedCt
    d { dctGoals :: [Goal]
    dctGoals = [Goal]
    without } else DelayedCt
    d

        _ -> Error
    err

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