    {-# LANGUAGE Safe #-}

    module Cryptol.TypeCheck.Default where

    import qualified Data.Set as Set
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe(mapMaybe, isJust)
    import Data.List((\\),nub)
    import Control.Monad(guard,mzero)

    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.SimpType(tMax)
    import Cryptol.TypeCheck.Error(Warning(..), Error(..))
    import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
    import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
    import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
    import Cryptol.Utils.Panic(panic)

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

    -- | We default constraints of the form @Literal t a@ and @FLiteral m n r a@.
    --
    --   For @Literal t a@ we examine the context of constraints on the type @a@
    --   to decide how to default.  If @Logic a@ is required,
    --   we cannot do any defaulting.  Otherwise, we default
    --   to either @Integer@ or @Rational@.  In particular, if
    --   we need to satisfy the @Field a@, constraint, we choose
    --   @Rational@ and otherwise we choose @Integer@.
    --
    --   For @FLiteral t a@ we always default to @Rational@.
    defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
    defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
    defaultLiterals [TVar]
    as [Goal]
    gs = let ([(TVar, Prop)]
    binds,[Warning]
    warns) = [((TVar, Prop), Warning)] -> ([(TVar, Prop)], [Warning])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ((TVar -> Maybe ((TVar, Prop), Warning))
    -> [TVar] -> [((TVar, Prop), Warning)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TVar -> Maybe ((TVar, Prop), Warning)
    tryDefVar [TVar]
    as)
                            in ([TVar]
    as [TVar] -> [TVar] -> [TVar]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ ((TVar, Prop) -> TVar) -> [(TVar, Prop)] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Prop) -> TVar
    forall a b. (a, b) -> a
    fst [(TVar, Prop)]
    binds, [(TVar, Prop)] -> Subst
    listSubst [(TVar, Prop)]
    binds, [Warning]
    warns)
      where
      gSet :: Goals
    gSet = [Goal] -> Goals
    goalsFromList [Goal]
    gs
      allProps :: Set Prop
    allProps = Goals -> Set Prop
    saturatedPropSet Goals
    gSet
      has :: (Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    p TVar
    a  = Prop -> Set Prop -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member (Prop -> Prop
    p (TVar -> Prop
    TVar TVar
    a)) Set Prop
    allProps

      isLiteralGoal :: TVar -> Bool
    isLiteralGoal TVar
    a = Maybe Goal -> Bool
    forall a. Maybe a -> Bool
    isJust (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)) Bool -> Bool -> Bool
    ||
                        Maybe Goal -> Bool
    forall a. Maybe a -> Bool
    isJust (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
    literalLessThanGoals Goals
    gSet))
      tryDefVar :: TVar -> Maybe ((TVar, Prop), Warning)
    tryDefVar TVar
    a =
        -- If there is an `FLiteral` constraint we use that for defaulting.
        case TVar
    -> Map TVar (Maybe ((TVar, Prop), Warning))
    -> Maybe (Maybe ((TVar, Prop), Warning))
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TVar
    a (Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
    flitDefaultCandidates Goals
    gSet) of
          Just Maybe ((TVar, Prop), Warning)
    m -> Maybe ((TVar, Prop), Warning)
    m

          -- Otherwise we try to use a `Literal`
          Maybe (Maybe ((TVar, Prop), Warning))
    Nothing
            | TVar -> Bool
    isLiteralGoal TVar
    a -> do
               Prop
    defT <- if (Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pLogic TVar
    a then Maybe Prop
    forall a. Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
                       else if (Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pField TVar
    a Bool -> Bool -> Bool
    && Bool -> Bool
    not ((Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pIntegral TVar
    a)
                              then Prop -> Maybe Prop
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Prop
    tRational
                       else if Bool -> Bool
    not ((Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pField TVar
    a) then Prop -> Maybe Prop
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Prop
    tInteger
                       else Maybe Prop
    forall a. Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
               let d :: TVarInfo
    d    = TVar -> TVarInfo
    tvInfo TVar
    a
                   w :: Warning
    w    = TVarInfo -> Prop -> Warning
    DefaultingTo TVarInfo
    d Prop
    defT
               Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member TVar
    a (Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Prop
    defT)))  -- Currently shouldn't happen
                                                      -- but future proofing.
               -- XXX: Make sure that `defT` has only variables that `a` is allowed
               -- to depend on
               ((TVar, Prop), Warning) -> Maybe ((TVar, Prop), Warning)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TVar
    a,Prop
    defT),Warning
    w)

            | Bool
    otherwise -> Maybe ((TVar, Prop), Warning)
    forall a. Maybe a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar,Type),Warning))
    flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar, Prop), Warning))
    flitDefaultCandidates Goals
    gs =
      [(TVar, Maybe ((TVar, Prop), Warning))]
    -> Map TVar (Maybe ((TVar, Prop), Warning))
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ((Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning)))
    -> [Goal] -> [(TVar, Maybe ((TVar, Prop), Warning))]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Goal -> Maybe (TVar, Maybe ((TVar, Prop), Warning))
    forall {m :: * -> *}.
    (Monad m, Alternative m) =>
    Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
    flitCandidate (Set Goal -> [Goal]
    forall a. Set a -> [a]
    Set.toList (Goals -> Set Goal
    goalSet Goals
    gs)))
      where
      allProps :: Set Prop
    allProps = Goals -> Set Prop
    saturatedPropSet Goals
    gs
      has :: (Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    p TVar
    a  = Prop -> Set Prop -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member (Prop -> Prop
    p (TVar -> Prop
    TVar TVar
    a)) Set Prop
    allProps

      flitCandidate :: Goal -> Maybe (TVar, m ((TVar, Prop), Warning))
    flitCandidate Goal
    g =
        do (Prop
    _,Prop
    _,Prop
    _,Prop
    x) <- Prop -> Maybe (Prop, Prop, Prop, Prop)
    pIsFLiteral (Goal -> Prop
    goal Goal
    g)
           TVar
    a         <- Prop -> Maybe TVar
    tIsVar Prop
    x
           (TVar, m ((TVar, Prop), Warning))
    -> Maybe (TVar, m ((TVar, Prop), Warning))
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TVar
    a, do Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not ((Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pLogic TVar
    a) Bool -> Bool -> Bool
    && Bool -> Bool
    not ((Prop -> Prop) -> TVar -> Bool
    has Prop -> Prop
    pIntegral TVar
    a))
                       let defT :: Prop
    defT = Prop
    tRational
                       let w :: Warning
    w    = TVarInfo -> Prop -> Warning
    DefaultingTo (TVar -> TVarInfo
    tvInfo TVar
    a) Prop
    defT
                       ((TVar, Prop), Warning) -> m ((TVar, Prop), Warning)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((TVar
    a,Prop
    defT),Warning
    w))

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

    -- This is what we use to avoid ambiguity when generalizing.

    {- If a variable, `a`, is:
        1. Of kind KNum
        2. Generic (i.e., does not appear in the environment)
        3. It appears only in constraints but not in the resulting type
           (i.e., it is not on the RHS of =>)
        4. It (say, the variable 'a') appears only in constraints like this:
            3.1 `a >= t` with (`a` not in `fvs t`)
            3.2 in the `s` of `fin s`

      Then we replace `a` with `max(t1 .. tn)` where the `ts`
      are from the constraints `a >= t`.

      If `t1 .. tn` is empty, then we replace `a` with 0.

      This function assumes that 1-3 have been checked, and implements the rest.
      So, given some variables and constraints that are about to be generalized,
      we return:
          1. a new (same or smaller) set of variables to quantify,
          2. a new set of constraints,
          3. a substitution which indicates what got defaulted.
    -}

    improveByDefaultingWithPure :: [TVar] -> [Goal] ->
        ( [TVar]    -- non-defaulted
        , [Goal]    -- new constraints
        , Subst     -- improvements from defaulting
        , [Error]   -- width defaulting errors
        )
    improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    improveByDefaultingWithPure [TVar]
    as [Goal]
    ps =
      Map TVar ([(Prop, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    classify ([(TVar, ([(Prop, Goal)], Set TVar))]
    -> Map TVar ([(Prop, Goal)], Set TVar)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (TVar
    a,([],Set TVar
    forall a. Set a
    Set.empty)) | TVar
    a <- [TVar]
    as ]) [] [] [Goal]
    ps

      where
      -- leq: candidate definitions (i.e. of the form x >= t, x `notElem` fvs t)
      --      for each of these, we keep the list of `t`, and the free vars in them.
      -- fins: all `fin` constraints
      -- others: any other constraints
      classify :: Map TVar ([(Prop, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    classify Map TVar ([(Prop, Goal)], Set TVar)
    leqs [Goal]
    fins [Goal]
    others [] =
        let -- First, we use the `leqs` to choose some definitions.
            ([(TVar, Prop)]
    defs, [Goal]
    newOthers)  = [(TVar, Prop)]
    -> [Goal]
    -> Set TVar
    -> [(TVar, ([(Prop, Goal)], Set TVar))]
    -> ([(TVar, Prop)], [Goal])
    forall {b}.
    TVars b =>
    [(TVar, Prop)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Prop, b)], Set TVar))]
    -> ([(TVar, Prop)], [b])
    select [] [] ([Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    others) (Map TVar ([(Prop, Goal)], Set TVar)
    -> [(TVar, ([(Prop, Goal)], Set TVar))]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map TVar ([(Prop, Goal)], Set TVar)
    leqs)
            su :: Subst
    su                 = [(TVar, Prop)] -> Subst
    listSubst [(TVar, Prop)]
    defs
            names :: Set TVar
    names              = Subst -> Set TVar
    substBinds Subst
    su
            mkErr :: (TVar, Prop) -> Error
    mkErr (TVar
    x,Prop
    t) =
              case TVar
    x of
                TVFree Int
    _ Kind
    _ Set TParam
    _ TVarInfo
    d
                  | Just Integer
    0 <- Prop -> Maybe Integer
    tIsNum Prop
    t -> TVarInfo -> Maybe Prop -> Error
    AmbiguousSize TVarInfo
    d Maybe Prop
    forall a. Maybe a
    Nothing
                  | Bool
    otherwise -> TVarInfo -> Maybe Prop -> Error
    AmbiguousSize TVarInfo
    d (Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    t)
                TVBound {} -> String -> [String] -> Error
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Crypto.TypeCheck.Infer"
                     [ String
    "tryDefault attempted to default a quantified variable."
                     ]

        in ( [ TVar
    a | TVar
    a <- [TVar]
    as, Bool -> Bool
    not (TVar
    a TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TVar
    names) ]
           , [Goal]
    newOthers [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++ [Goal]
    others [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++ [Goal] -> [Goal]
    forall a. Eq a => [a] -> [a]
    nub (Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su [Goal]
    fins)
           , Subst
    su
           , ((TVar, Prop) -> Error) -> [(TVar, Prop)] -> [Error]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Prop) -> Error
    mkErr [(TVar, Prop)]
    defs
           )

      classify Map TVar ([(Prop, Goal)], Set TVar)
    leqs [Goal]
    fins [Goal]
    others (Goal
    prop : [Goal]
    more) =
          case Prop -> Prop
    tNoUser (Goal -> Prop
    goal Goal
    prop) of

            -- We found a `fin` constraint.
            TCon (PC PC
    PFin) [ Prop
    _ ] -> Map TVar ([(Prop, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    classify Map TVar ([(Prop, Goal)], Set TVar)
    leqs (Goal
    prop Goal -> [Goal] -> [Goal]
    forall a. a -> [a] -> [a]
    : [Goal]
    fins) [Goal]
    others [Goal]
    more

            -- Things of the form: x >= T(x) are not defaulted.
            TCon (PC PC
    PGeq) [ TVar TVar
    x, Prop
    t ]
              | TVar
    x TVar -> [TVar] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TVar]
    as Bool -> Bool -> Bool
    && TVar
    x TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.notMember` Set TVar
    freeRHS ->
               Map TVar ([(Prop, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    classify Map TVar ([(Prop, Goal)], Set TVar)
    leqs' [Goal]
    fins [Goal]
    others [Goal]
    more
               where freeRHS :: Set TVar
    freeRHS = Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Prop
    t
                     add :: ([a], Set a) -> ([a], Set a) -> ([a], Set a)
    add ([a]
    xs1,Set a
    vs1) ([a]
    xs2,Set a
    vs2) = ([a]
    xs1 [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a]
    xs2, Set a -> Set a -> Set a
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set a
    vs1 Set a
    vs2)
                     leqs' :: Map TVar ([(Prop, Goal)], Set TVar)
    leqs' = (([(Prop, Goal)], Set TVar)
     -> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar))
    -> TVar
    -> ([(Prop, Goal)], Set TVar)
    -> Map TVar ([(Prop, Goal)], Set TVar)
    -> Map TVar ([(Prop, Goal)], Set TVar)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith ([(Prop, Goal)], Set TVar)
    -> ([(Prop, Goal)], Set TVar) -> ([(Prop, Goal)], Set TVar)
    forall {a} {a}.
    Ord a =>
    ([a], Set a) -> ([a], Set a) -> ([a], Set a)
    add TVar
    x ([(Prop
    t,Goal
    prop)],Set TVar
    freeRHS) Map TVar ([(Prop, Goal)], Set TVar)
    leqs

            Prop
    _ -> Map TVar ([(Prop, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Error])
    classify Map TVar ([(Prop, Goal)], Set TVar)
    leqs [Goal]
    fins (Goal
    prop Goal -> [Goal] -> [Goal]
    forall a. a -> [a] -> [a]
    : [Goal]
    others) [Goal]
    more

      -- Pickout which variables may be defaulted and how.
        -- XXX: simpType t
      select :: [(TVar, Prop)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Prop, b)], Set TVar))]
    -> ([(TVar, Prop)], [b])
    select [(TVar, Prop)]
    yes [b]
    no Set TVar
    _ [] = ([ (TVar
    x, Prop
    t) | (TVar
    x,Prop
    t) <- [(TVar, Prop)]
    yes ] ,[b]
    no)
      select [(TVar, Prop)]
    yes [b]
    no Set TVar
    otherFree ((TVar
    x,([(Prop, b)]
    rhsG,Set TVar
    vs)) : [(TVar, ([(Prop, b)], Set TVar))]
    more) =
        [(TVar, Prop)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Prop, b)], Set TVar))]
    -> ([(TVar, Prop)], [b])
    select [(TVar, Prop)]
    newYes [b]
    newNo Set TVar
    newFree [(TVar, ([(Prop, b)], Set TVar))]
    newMore

        where
        ([Prop]
    ts,[b]
    gs) = [(Prop, b)] -> ([Prop], [b])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(Prop, b)]
    rhsG

        -- `x` selected only if appears nowehere else.
        -- this includes other candidates for defaulting.
        ([(TVar, Prop)]
    newYes,[b]
    newNo,Set TVar
    newFree,[(TVar, ([(Prop, b)], Set TVar))]
    newMore)

            -- Mentioned in other constraints, definately not defaultable.
            | TVar
    x TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TVar
    otherFree = ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
    noDefaulting

            | Bool
    otherwise =
                let deps :: [TVar]
    deps = [ TVar
    y | (TVar
    y,([(Prop, b)]
    _,Set TVar
    yvs)) <- [(TVar, ([(Prop, b)], Set TVar))]
    more, TVar
    x TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TVar
    yvs ]
                    recs :: [TVar]
    recs = (TVar -> Bool) -> [TVar] -> [TVar]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (TVar -> Set TVar -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TVar
    vs) [TVar]
    deps
                in if Bool -> Bool
    not ([TVar] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TVar]
    recs) Bool -> Bool -> Bool
    || TVar -> Bool
    isBoundTV TVar
    x -- x >= S(y), y >= T(x)
                                     then ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
    noDefaulting

                                      -- x >= S,    y >= T(x)   or
                                      -- x >= S(y), y >= S
                                      else ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
    yesDefaulting

            where
            noDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
    noDefaulting = ( [(TVar, Prop)]
    yes, [b]
    gs [b] -> [b] -> [b]
    forall a. [a] -> [a] -> [a]
    ++ [b]
    no, Set TVar
    vs Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set TVar
    otherFree, [(TVar, ([(Prop, b)], Set TVar))]
    more )

            yesDefaulting :: ([(TVar, Prop)], [b], Set TVar, [(TVar, ([(Prop, b)], Set TVar))])
    yesDefaulting =
              let ty :: Prop
    ty  = case [Prop]
    ts of
                          [] -> Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (Int
    0::Int)
                          [Prop]
    _  -> (Prop -> Prop -> Prop) -> [Prop] -> Prop
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Prop -> Prop -> Prop
    tMax [Prop]
    ts
                  su1 :: Subst
    su1 = TVar -> Prop -> Subst
    uncheckedSingleSubst TVar
    x Prop
    ty
              in ( (TVar
    x,Prop
    ty) (TVar, Prop) -> [(TVar, Prop)] -> [(TVar, Prop)]
    forall a. a -> [a] -> [a]
    : [ (TVar
    y,Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 Prop
    t) | (TVar
    y,Prop
    t) <- [(TVar, Prop)]
    yes ]
                 , [b]
    no         -- We know that `x` does not appear here
                 , Set TVar
    otherFree  -- We know that `x` did not appear here either

                 -- No need to update the `vs` because we've already
                 -- checked that there are no recursive dependencies.
                 , [ (TVar
    y, (Subst -> [(Prop, b)] -> [(Prop, b)]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 [(Prop, b)]
    ts1, Set TVar
    vs1)) | (TVar
    y,([(Prop, b)]
    ts1,Set TVar
    vs1)) <- [(TVar, ([(Prop, b)], Set TVar))]
    more ]
                 )

    {- | Try to pick a reasonable instantiation for an expression with
    the given type.  This is useful when we do evaluation at the REPL.
    The resulting types should satisfy the constraints of the schema.
    The parameters should be all of numeric kind, and the props should als
    be numeric -}
    defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [ (TParam,Type) ])
    defaultReplExpr' :: Solver -> [TParam] -> [Prop] -> IO (Maybe [(TParam, Prop)])
    defaultReplExpr' Solver
    sol [TParam]
    as [Prop]
    props =
      do let params :: [TVar]
    params = (TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar [TParam]
    as
         Maybe [(TVar, Nat')]
    mb <- Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])
    tryGetModel Solver
    sol [TVar]
    params [Prop]
    props
         case Maybe [(TVar, Nat')]
    mb of
           Maybe [(TVar, Nat')]
    Nothing -> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [(TParam, Prop)]
    forall a. Maybe a
    Nothing
           Just [(TVar, Nat')]
    mdl0 ->
             do [(TVar, Nat')]
    mdl <- Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
    shrinkModel Solver
    sol [TVar]
    params [Prop]
    props [(TVar, Nat')]
    mdl0
                let su :: Subst
    su = [(TVar, Prop)] -> Subst
    listSubst [ (TVar
    x, Nat' -> Prop
    tNat' Nat'
    n) | (TVar
    x,Nat'
    n) <- [(TVar, Nat')]
    mdl ]
                Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)]))
    -> Maybe [(TParam, Prop)] -> IO (Maybe [(TParam, Prop)])
    forall a b. (a -> b) -> a -> b
    $
                  do Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ([Prop] -> Bool
    forall a. [a] -> 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 [Prop]
    props)))
                     [Prop]
    tys <- (TVar -> Maybe Prop) -> [TVar] -> Maybe [Prop]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Subst -> TVar -> Maybe Prop
    forall {m :: * -> *}.
    (Monad m, Alternative m) =>
    Subst -> TVar -> m Prop
    bindParam Subst
    su) [TVar]
    params
                     [(TParam, Prop)] -> Maybe [(TParam, Prop)]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam] -> [Prop] -> [(TParam, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TParam]
    as [Prop]
    tys)
      where
      bindParam :: Subst -> TVar -> m Prop
    bindParam Subst
    su TVar
    tp =
        do let ty :: Prop
    ty  = TVar -> Prop
    TVar TVar
    tp
               ty' :: Prop
    ty' = Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Prop
    ty
           Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Prop
    ty Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Prop
    ty')
           Prop -> m Prop
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Prop
    ty'