    module Cryptol.TypeCheck.Default where

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

    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.SimpType(tMax,tWidth)
    import Cryptol.TypeCheck.Error(Warning(..))
    import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
    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@ to @a := [width t]@
    defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
    defaultLiterals :: [TVar] -> [Goal] -> ([TVar], Subst, [Warning])
    defaultLiterals as :: [TVar]
    as gs :: [Goal]
    gs = let (binds :: [(TVar, Type)]
    binds,warns :: [Warning]
    warns) = [((TVar, Type), Warning)] -> ([(TVar, Type)], [Warning])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ((TVar -> Maybe ((TVar, Type), Warning))
    -> [TVar] -> [((TVar, Type), Warning)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TVar -> Maybe ((TVar, Type), Warning)
    tryDefVar [TVar]
    as)
                            in ([TVar]
    as [TVar] -> [TVar] -> [TVar]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ ((TVar, Type) -> TVar) -> [(TVar, Type)] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Type) -> TVar
    forall a b. (a, b) -> a
    fst [(TVar, Type)]
    binds, [(TVar, Type)] -> Subst
    listSubst [(TVar, Type)]
    binds, [Warning]
    warns)
      where
      gSet :: Goals
    gSet = [Goal] -> Goals
    goalsFromList [Goal]
    gs
      tryDefVar :: TVar -> Maybe ((TVar, Type), Warning)
    tryDefVar a :: TVar
    a =
        do 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 d :: TVarInfo
    d    = TVar -> TVarInfo
    tvInfo TVar
    a
               defT :: Type
    defT = Type -> Type
    tWord (Type -> Type
    tWidth (Goal -> Type
    goal Goal
    gt))
               w :: Warning
    w    = TVarInfo -> Type -> Warning
    DefaultingTo TVarInfo
    d Type
    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 (Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    defT)))  -- Currently shouldn't happen
                                                  -- but future proofing.
           -- XXX: Make sure that `defT` has only variables that `a` is allowed
           -- to depend on
           ((TVar, Type), Warning) -> Maybe ((TVar, Type), Warning)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TVar
    a,Type
    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
        , [Warning] -- warnings about defaulting
        )
    improveByDefaultingWithPure :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    improveByDefaultingWithPure as :: [TVar]
    as ps :: [Goal]
    ps =
      Map TVar ([(Type, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    classify ([(TVar, ([(Type, Goal)], Set TVar))]
    -> Map TVar ([(Type, 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 ([(Type, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    classify leqs :: Map TVar ([(Type, Goal)], Set TVar)
    leqs fins :: [Goal]
    fins others :: [Goal]
    others [] =
        let -- First, we use the `leqs` to choose some definitions.
            (defs :: [(TVar, Type)]
    defs, newOthers :: [Goal]
    newOthers)  = [(TVar, Type)]
    -> [Goal]
    -> Set TVar
    -> [(TVar, ([(Type, Goal)], Set TVar))]
    -> ([(TVar, Type)], [Goal])
    forall b.
    TVars b =>
    [(TVar, Type)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Type, b)], Set TVar))]
    -> ([(TVar, Type)], [b])
    select [] [] ([Goal] -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs [Goal]
    others) (Map TVar ([(Type, Goal)], Set TVar)
    -> [(TVar, ([(Type, Goal)], Set TVar))]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map TVar ([(Type, Goal)], Set TVar)
    leqs)
            su :: Subst
    su                 = [(TVar, Type)] -> Subst
    listSubst [(TVar, Type)]
    defs
            warn :: (TVar, Type) -> Warning
    warn (x :: TVar
    x,t :: Type
    t) =
              case TVar
    x of
                TVFree _ _ _ d :: TVarInfo
    d -> TVarInfo -> Type -> Warning
    DefaultingTo TVarInfo
    d Type
    t
                TVBound {} -> String -> [String] -> Warning
    forall a. HasCallStack => String -> [String] -> a
    panic "Crypto.TypeCheck.Infer"
                     [ "tryDefault attempted to default a quantified variable."
                     ]

            names :: Set TVar
    names = Subst -> Set TVar
    substBinds Subst
    su

        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, Type) -> Warning) -> [(TVar, Type)] -> [Warning]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Type) -> Warning
    warn [(TVar, Type)]
    defs
           )

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

            -- We found a `fin` constraint.
            TCon (PC PFin) [ _ ] -> Map TVar ([(Type, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    classify Map TVar ([(Type, 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 PGeq) [ TVar x :: TVar
    x, t :: Type
    t ]
              | TVar
    x TVar -> [TVar] -> 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 ([(Type, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    classify Map TVar ([(Type, Goal)], Set TVar)
    leqs' [Goal]
    fins [Goal]
    others [Goal]
    more
               where freeRHS :: Set TVar
    freeRHS = Type -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs Type
    t
                     add :: ([a], Set a) -> ([a], Set a) -> ([a], Set a)
    add (xs1 :: [a]
    xs1,vs1 :: Set a
    vs1) (xs2 :: [a]
    xs2,vs2 :: 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 ([(Type, Goal)], Set TVar)
    leqs' = (([(Type, Goal)], Set TVar)
     -> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar))
    -> TVar
    -> ([(Type, Goal)], Set TVar)
    -> Map TVar ([(Type, Goal)], Set TVar)
    -> Map TVar ([(Type, Goal)], Set TVar)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith ([(Type, Goal)], Set TVar)
    -> ([(Type, Goal)], Set TVar) -> ([(Type, Goal)], Set TVar)
    forall a a. Ord a => ([a], Set a) -> ([a], Set a) -> ([a], Set a)
    add TVar
    x ([(Type
    t,Goal
    prop)],Set TVar
    freeRHS) Map TVar ([(Type, Goal)], Set TVar)
    leqs

            _ -> Map TVar ([(Type, Goal)], Set TVar)
    -> [Goal] -> [Goal] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
    classify Map TVar ([(Type, 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, Type)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Type, b)], Set TVar))]
    -> ([(TVar, Type)], [b])
    select yes :: [(TVar, Type)]
    yes no :: [b]
    no _ [] = ([ (TVar
    x, Type
    t) | (x :: TVar
    x,t :: Type
    t) <- [(TVar, Type)]
    yes ] ,[b]
    no)
      select yes :: [(TVar, Type)]
    yes no :: [b]
    no otherFree :: Set TVar
    otherFree ((x :: TVar
    x,(rhsG :: [(Type, b)]
    rhsG,vs :: Set TVar
    vs)) : more :: [(TVar, ([(Type, b)], Set TVar))]
    more) =
        [(TVar, Type)]
    -> [b]
    -> Set TVar
    -> [(TVar, ([(Type, b)], Set TVar))]
    -> ([(TVar, Type)], [b])
    select [(TVar, Type)]
    newYes [b]
    newNo Set TVar
    newFree [(TVar, ([(Type, b)], Set TVar))]
    newMore

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

        -- `x` selected only if appears nowehere else.
        -- this includes other candidates for defaulting.
        (newYes :: [(TVar, Type)]
    newYes,newNo :: [b]
    newNo,newFree :: Set TVar
    newFree,newMore :: [(TVar, ([(Type, 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, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
    noDefaulting

            | Bool
    otherwise =
                let deps :: [TVar]
    deps = [ TVar
    y | (y :: TVar
    y,(_,yvs :: Set TVar
    yvs)) <- [(TVar, ([(Type, 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 (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, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
    noDefaulting

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

            where
            noDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
    noDefaulting = ( [(TVar, Type)]
    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, ([(Type, b)], Set TVar))]
    more )

            yesDefaulting :: ([(TVar, Type)], [b], Set TVar, [(TVar, ([(Type, b)], Set TVar))])
    yesDefaulting =
              let ty :: Type
    ty  = case [Type]
    ts of
                          [] -> Int -> Type
    forall a. Integral a => a -> Type
    tNum (0::Int)
                          _  -> (Type -> Type -> Type) -> [Type] -> Type
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Type -> Type -> Type
    tMax [Type]
    ts
                  su1 :: Subst
    su1 = TVar -> Type -> Subst
    singleSubst TVar
    x Type
    ty
              in ( (TVar
    x,Type
    ty) (TVar, Type) -> [(TVar, Type)] -> [(TVar, Type)]
    forall a. a -> [a] -> [a]
    : [ (TVar
    y,Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 Type
    t) | (y :: TVar
    y,t :: Type
    t) <- [(TVar, Type)]
    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 -> [(Type, b)] -> [(Type, b)]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su1 [(Type, b)]
    ts1, Set TVar
    vs1)) | (y :: TVar
    y,(ts1 :: [(Type, b)]
    ts1,vs1 :: Set TVar
    vs1)) <- [(TVar, ([(Type, 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] -> [Type] -> IO (Maybe [(TParam, Type)])
    defaultReplExpr' sol :: Solver
    sol as :: [TParam]
    as props :: [Type]
    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] -> [Type] -> IO (Maybe [(TVar, Nat')])
    tryGetModel Solver
    sol [TVar]
    params [Type]
    props
         case Maybe [(TVar, Nat')]
    mb of
           Nothing -> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [(TParam, Type)]
    forall a. Maybe a
    Nothing
           Just mdl0 :: [(TVar, Nat')]
    mdl0 ->
             do [(TVar, Nat')]
    mdl <- Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
    shrinkModel Solver
    sol [TVar]
    params [Type]
    props [(TVar, Nat')]
    mdl0
                let su :: Subst
    su = [(TVar, Type)] -> Subst
    listSubst [ (TVar
    x, Nat' -> Type
    tNat' Nat'
    n) | (x :: TVar
    x,n :: Nat'
    n) <- [(TVar, Nat')]
    mdl ]
                Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)]))
    -> Maybe [(TParam, Type)] -> IO (Maybe [(TParam, Type)])
    forall a b. (a -> b) -> a -> b
    $
                  do Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ([Type] -> 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 [Type]
    props)))
                     [Type]
    tys <- (TVar -> Maybe Type) -> [TVar] -> Maybe [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Subst -> TVar -> Maybe Type
    forall (m :: * -> *).
    (Monad m, Alternative m) =>
    Subst -> TVar -> m Type
    bindParam Subst
    su) [TVar]
    params
                     [(TParam, Type)] -> Maybe [(TParam, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([TParam] -> [Type] -> [(TParam, Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TParam]
    as [Type]
    tys)
      where
      bindParam :: Subst -> TVar -> m Type
    bindParam su :: Subst
    su tp :: TVar
    tp =
        do let ty :: Type
    ty  = TVar -> Type
    TVar TVar
    tp
               ty' :: Type
    ty' = Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Type
    ty
           Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Type
    ty Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Type
    ty')
           Type -> m Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ty'