    -- |
    -- Module      :  Cryptol.TypeCheck.InferTypes
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- This module contains types used during type inference.

    {-# LANGUAGE Safe #-}

    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE ViewPatterns #-}
    module Cryptol.TypeCheck.InferTypes where

    import           Cryptol.Parser.Position
    import           Cryptol.ModuleSystem.Name (asPrim,nameLoc)
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.PP
    import           Cryptol.TypeCheck.Subst
    import           Cryptol.TypeCheck.TypePat
    import           Cryptol.TypeCheck.SimpType(tMax)
    import           Cryptol.Utils.Ident (ModName, identText)
    import           Cryptol.Utils.Panic(panic)
    import           Cryptol.Utils.Misc(anyJust)
    import           Cryptol.Utils.Patterns(matchMaybe)

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

    import GHC.Generics (Generic)
    import Control.DeepSeq

    data SolverConfig = SolverConfig
      { SolverConfig -> FilePath
    solverPath    :: FilePath   -- ^ The SMT solver to invoke
      , SolverConfig -> [FilePath]
    solverArgs    :: [String]   -- ^ Additional arguments to pass to the solver
      , SolverConfig -> Int
    solverVerbose :: Int        -- ^ How verbose to be when type-checking
      , SolverConfig -> [FilePath]
    solverPreludePath :: [FilePath]
        -- ^ Look for the solver prelude in these locations.
      } deriving (Int -> SolverConfig -> ShowS
    [SolverConfig] -> ShowS
    SolverConfig -> FilePath
    (Int -> SolverConfig -> ShowS)
    -> (SolverConfig -> FilePath)
    -> ([SolverConfig] -> ShowS)
    -> Show SolverConfig
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [SolverConfig] -> ShowS
    $cshowList :: [SolverConfig] -> ShowS
    show :: SolverConfig -> FilePath
    $cshow :: SolverConfig -> FilePath
    showsPrec :: Int -> SolverConfig -> ShowS
    $cshowsPrec :: Int -> SolverConfig -> ShowS
    Show, (forall x. SolverConfig -> Rep SolverConfig x)
    -> (forall x. Rep SolverConfig x -> SolverConfig)
    -> Generic SolverConfig
    forall x. Rep SolverConfig x -> SolverConfig
    forall x. SolverConfig -> Rep SolverConfig x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep SolverConfig x -> SolverConfig
    $cfrom :: forall x. SolverConfig -> Rep SolverConfig x
    Generic, SolverConfig -> ()
    (SolverConfig -> ()) -> NFData SolverConfig
    forall a. (a -> ()) -> NFData a
    rnf :: SolverConfig -> ()
    $crnf :: SolverConfig -> ()
    NFData)

    -- | The types of variables in the environment.
    data VarType = ExtVar Schema
                   -- ^ Known type

                 | CurSCC {- LAZY -} Expr Type
                   {- ^ Part of current SCC.  The expression will replace the
                   variable, after we are done with the SCC.  In this way a
                   variable that gets generalized is replaced with an appropriate
                   instantiation of itself. -}

    data Goals = Goals
      { Goals -> Set Goal
    goalSet :: Set Goal
        -- ^ A bunch of goals, not including the ones in 'literalGoals'.

      , Goals -> Map TVar Goal
    literalGoals :: Map TVar LitGoal
        -- ^ An entry @(a,t)@ corresponds to @Literal t a@.
      } deriving (Int -> Goals -> ShowS
    [Goals] -> ShowS
    Goals -> FilePath
    (Int -> Goals -> ShowS)
    -> (Goals -> FilePath) -> ([Goals] -> ShowS) -> Show Goals
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [Goals] -> ShowS
    $cshowList :: [Goals] -> ShowS
    show :: Goals -> FilePath
    $cshow :: Goals -> FilePath
    showsPrec :: Int -> Goals -> ShowS
    $cshowsPrec :: Int -> Goals -> ShowS
    Show)

    -- | This abuses the type 'Goal' a bit. The 'goal' field contains
    -- only the numeric part of the Literal constraint.  For example,
    -- @(a, Goal { goal = t })@ representats the goal for @Literal t a@
    type LitGoal = Goal

    litGoalToGoal :: (TVar,LitGoal) -> Goal
    litGoalToGoal :: (TVar, Goal) -> Goal
    litGoalToGoal (a :: TVar
    a,g :: Goal
    g) = Goal
    g { goal :: Prop
    goal = Prop -> Prop -> Prop
    pLiteral (Goal -> Prop
    goal Goal
    g) (TVar -> Prop
    TVar TVar
    a) }

    goalToLitGoal :: Goal -> Maybe (TVar,LitGoal)
    goalToLitGoal :: Goal -> Maybe (TVar, Goal)
    goalToLitGoal g :: Goal
    g =
      do (tn :: Prop
    tn,a :: TVar
    a) <- Match (Prop, TVar) -> Maybe (Prop, TVar)
    forall a. Match a -> Maybe a
    matchMaybe (Match (Prop, TVar) -> Maybe (Prop, TVar))
    -> Match (Prop, TVar) -> Maybe (Prop, TVar)
    forall a b. (a -> b) -> a -> b
    $ do (tn :: Prop
    tn,b :: Prop
    b) <- Pat Prop (Prop, Prop)
    aLiteral (Goal -> Prop
    goal Goal
    g)
                                   TVar
    a      <- Pat Prop TVar
    aTVar Prop
    b
                                   (Prop, TVar) -> Match (Prop, TVar)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Prop
    tn,TVar
    a)
         (TVar, Goal) -> Maybe (TVar, Goal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    a, Goal
    g { goal :: Prop
    goal = Prop
    tn })

    emptyGoals :: Goals
    emptyGoals :: Goals
    emptyGoals  = Goals :: Set Goal -> Map TVar Goal -> Goals
    Goals { goalSet :: Set Goal
    goalSet = Set Goal
    forall a. Set a
    Set.empty, literalGoals :: Map TVar Goal
    literalGoals = Map TVar Goal
    forall k a. Map k a
    Map.empty }

    nullGoals :: Goals -> Bool
    nullGoals :: Goals -> Bool
    nullGoals gs :: Goals
    gs = Set Goal -> Bool
    forall a. Set a -> Bool
    Set.null (Goals -> Set Goal
    goalSet Goals
    gs) Bool -> Bool -> Bool
    && Map TVar Goal -> Bool
    forall k a. Map k a -> Bool
    Map.null (Goals -> Map TVar Goal
    literalGoals Goals
    gs)

    fromGoals :: Goals -> [Goal]
    fromGoals :: Goals -> [Goal]
    fromGoals gs :: Goals
    gs = ((TVar, Goal) -> Goal) -> [(TVar, Goal)] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar, Goal) -> Goal
    litGoalToGoal (Map TVar Goal -> [(TVar, Goal)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Goals -> Map TVar Goal
    literalGoals Goals
    gs)) [Goal] -> [Goal] -> [Goal]
    forall a. [a] -> [a] -> [a]
    ++
                   Set Goal -> [Goal]
    forall a. Set a -> [a]
    Set.toList (Goals -> Set Goal
    goalSet Goals
    gs)

    goalsFromList :: [Goal] -> Goals
    goalsFromList :: [Goal] -> Goals
    goalsFromList = (Goal -> Goals -> Goals) -> Goals -> [Goal] -> Goals
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Goal -> Goals -> Goals
    insertGoal Goals
    emptyGoals

    insertGoal :: Goal -> Goals -> Goals
    insertGoal :: Goal -> Goals -> Goals
    insertGoal g :: Goal
    g gs :: Goals
    gs
      | Just (a :: TVar
    a,newG :: Goal
    newG) <- Goal -> Maybe (TVar, Goal)
    goalToLitGoal Goal
    g =
                    Goals
    gs { literalGoals :: Map TVar Goal
    literalGoals = (Goal -> Goal -> Goal)
    -> TVar -> Goal -> Map TVar Goal -> Map TVar Goal
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Goal -> Goal -> Goal
    jn TVar
    a Goal
    newG (Goals -> Map TVar Goal
    literalGoals Goals
    gs) }
      | Bool
    otherwise = Goals
    gs { goalSet :: Set Goal
    goalSet = Goal -> Set Goal -> Set Goal
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Goal
    g (Goals -> Set Goal
    goalSet Goals
    gs) }

      where
      jn :: Goal -> Goal -> Goal
    jn g1 :: Goal
    g1 g2 :: Goal
    g2 = Goal
    g1 { goal :: Prop
    goal = Prop -> Prop -> Prop
    tMax (Goal -> Prop
    goal Goal
    g1) (Goal -> Prop
    goal Goal
    g2) }
      -- XXX: here we are arbitrarily using the info of the first goal,
      -- which could lead to a confusing location for a constraint.

    -- | Something that we need to find evidence for.
    data Goal = Goal
      { Goal -> ConstraintSource
    goalSource :: ConstraintSource  -- ^ What it is about
      , Goal -> Range
    goalRange  :: Range             -- ^ Part of source code that caused goal
      , Goal -> Prop
    goal       :: Prop              -- ^ What needs to be proved
      } deriving (Int -> Goal -> ShowS
    [Goal] -> ShowS
    Goal -> FilePath
    (Int -> Goal -> ShowS)
    -> (Goal -> FilePath) -> ([Goal] -> ShowS) -> Show Goal
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [Goal] -> ShowS
    $cshowList :: [Goal] -> ShowS
    show :: Goal -> FilePath
    $cshow :: Goal -> FilePath
    showsPrec :: Int -> Goal -> ShowS
    $cshowsPrec :: Int -> Goal -> ShowS
    Show, (forall x. Goal -> Rep Goal x)
    -> (forall x. Rep Goal x -> Goal) -> Generic Goal
    forall x. Rep Goal x -> Goal
    forall x. Goal -> Rep Goal x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Goal x -> Goal
    $cfrom :: forall x. Goal -> Rep Goal x
    Generic, Goal -> ()
    (Goal -> ()) -> NFData Goal
    forall a. (a -> ()) -> NFData a
    rnf :: Goal -> ()
    $crnf :: Goal -> ()
    NFData)

    instance Eq Goal where
      x :: Goal
    x == :: Goal -> Goal -> Bool
    == y :: Goal
    y = Goal -> Prop
    goal Goal
    x Prop -> Prop -> Bool
    forall a. Eq a => a -> a -> Bool
    == Goal -> Prop
    goal Goal
    y

    instance Ord Goal where
      compare :: Goal -> Goal -> Ordering
    compare x :: Goal
    x y :: Goal
    y = Prop -> Prop -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Goal -> Prop
    goal Goal
    x) (Goal -> Prop
    goal Goal
    y)

    data HasGoal = HasGoal
      { HasGoal -> Int
    hasName :: !Int
      , HasGoal -> Goal
    hasGoal :: Goal
      } deriving Int -> HasGoal -> ShowS
    [HasGoal] -> ShowS
    HasGoal -> FilePath
    (Int -> HasGoal -> ShowS)
    -> (HasGoal -> FilePath) -> ([HasGoal] -> ShowS) -> Show HasGoal
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [HasGoal] -> ShowS
    $cshowList :: [HasGoal] -> ShowS
    show :: HasGoal -> FilePath
    $cshow :: HasGoal -> FilePath
    showsPrec :: Int -> HasGoal -> ShowS
    $cshowsPrec :: Int -> HasGoal -> ShowS
    Show

    -- | A solution for a 'HasGoal'
    data HasGoalSln = HasGoalSln
      { HasGoalSln -> Expr -> Expr
    hasDoSelect :: Expr -> Expr
        -- ^ Select a specific field from the input expsression.

      , HasGoalSln -> Expr -> Expr -> Expr
    hasDoSet    :: Expr -> Expr -> Expr
        -- ^ Set a field of the first expression to the second expression
      }

    -- | Delayed implication constraints, arising from user-specified type sigs.
    data DelayedCt = DelayedCt
      { DelayedCt -> Maybe Name
    dctSource :: Maybe Name   -- ^ Signature that gave rise to this constraint
                                  -- Nothing means module top-level
      , DelayedCt -> [TParam]
    dctForall :: [TParam]
      , DelayedCt -> [Prop]
    dctAsmps  :: [Prop]
      , DelayedCt -> [Goal]
    dctGoals  :: [Goal]
      } deriving (Int -> DelayedCt -> ShowS
    [DelayedCt] -> ShowS
    DelayedCt -> FilePath
    (Int -> DelayedCt -> ShowS)
    -> (DelayedCt -> FilePath)
    -> ([DelayedCt] -> ShowS)
    -> Show DelayedCt
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [DelayedCt] -> ShowS
    $cshowList :: [DelayedCt] -> ShowS
    show :: DelayedCt -> FilePath
    $cshow :: DelayedCt -> FilePath
    showsPrec :: Int -> DelayedCt -> ShowS
    $cshowsPrec :: Int -> DelayedCt -> ShowS
    Show, (forall x. DelayedCt -> Rep DelayedCt x)
    -> (forall x. Rep DelayedCt x -> DelayedCt) -> Generic DelayedCt
    forall x. Rep DelayedCt x -> DelayedCt
    forall x. DelayedCt -> Rep DelayedCt x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep DelayedCt x -> DelayedCt
    $cfrom :: forall x. DelayedCt -> Rep DelayedCt x
    Generic, DelayedCt -> ()
    (DelayedCt -> ()) -> NFData DelayedCt
    forall a. (a -> ()) -> NFData a
    rnf :: DelayedCt -> ()
    $crnf :: DelayedCt -> ()
    NFData)

    -- | Information about how a constraint came to be, used in error reporting.
    data ConstraintSource
      = CtComprehension       -- ^ Computing shape of list comprehension
      | CtSplitPat            -- ^ Use of a split pattern
      | CtTypeSig             -- ^ A type signature in a pattern or expression
      | CtInst Expr           -- ^ Instantiation of this expression
      | CtSelector
      | CtExactType
      | CtEnumeration
      | CtDefaulting          -- ^ Just defaulting on the command line
      | CtPartialTypeFun Name -- ^ Use of a partial type function.
      | CtImprovement
      | CtPattern Doc         -- ^ Constraints arising from type-checking patterns
      | CtModuleInstance ModName -- ^ Instantiating a parametrized module
        deriving (Int -> ConstraintSource -> ShowS
    [ConstraintSource] -> ShowS
    ConstraintSource -> FilePath
    (Int -> ConstraintSource -> ShowS)
    -> (ConstraintSource -> FilePath)
    -> ([ConstraintSource] -> ShowS)
    -> Show ConstraintSource
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [ConstraintSource] -> ShowS
    $cshowList :: [ConstraintSource] -> ShowS
    show :: ConstraintSource -> FilePath
    $cshow :: ConstraintSource -> FilePath
    showsPrec :: Int -> ConstraintSource -> ShowS
    $cshowsPrec :: Int -> ConstraintSource -> ShowS
    Show, (forall x. ConstraintSource -> Rep ConstraintSource x)
    -> (forall x. Rep ConstraintSource x -> ConstraintSource)
    -> Generic ConstraintSource
    forall x. Rep ConstraintSource x -> ConstraintSource
    forall x. ConstraintSource -> Rep ConstraintSource x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep ConstraintSource x -> ConstraintSource
    $cfrom :: forall x. ConstraintSource -> Rep ConstraintSource x
    Generic, ConstraintSource -> ()
    (ConstraintSource -> ()) -> NFData ConstraintSource
    forall a. (a -> ()) -> NFData a
    rnf :: ConstraintSource -> ()
    $crnf :: ConstraintSource -> ()
    NFData)

    instance TVars ConstraintSource where
      apSubst :: Subst -> ConstraintSource -> ConstraintSource
    apSubst su :: Subst
    su src :: ConstraintSource
    src =
        case ConstraintSource
    src of
          CtComprehension -> ConstraintSource
    src
          CtSplitPat      -> ConstraintSource
    src
          CtTypeSig       -> ConstraintSource
    src
          CtInst e :: Expr
    e        -> Expr -> ConstraintSource
    CtInst (Subst -> Expr -> Expr
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su Expr
    e)
          CtSelector      -> ConstraintSource
    src
          CtExactType     -> ConstraintSource
    src
          CtEnumeration   -> ConstraintSource
    src
          CtDefaulting    -> ConstraintSource
    src
          CtPartialTypeFun _ -> ConstraintSource
    src
          CtImprovement    -> ConstraintSource
    src
          CtPattern _      -> ConstraintSource
    src
          CtModuleInstance _ -> ConstraintSource
    src

    instance FVS Goal where
      fvs :: Goal -> Set TVar
    fvs g :: Goal
    g = Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Goal -> Prop
    goal Goal
    g)

    instance FVS DelayedCt where
      fvs :: DelayedCt -> Set TVar
    fvs d :: DelayedCt
    d = ([Prop], [Goal]) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (DelayedCt -> [Prop]
    dctAsmps DelayedCt
    d, DelayedCt -> [Goal]
    dctGoals DelayedCt
    d) Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference`
                                [TVar] -> Set TVar
    forall a. Ord a => [a] -> Set a
    Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar (DelayedCt -> [TParam]
    dctForall DelayedCt
    d))

    instance TVars Goals where
      -- XXX: could be more efficient
      apSubst :: Subst -> Goals -> Goals
    apSubst su :: Subst
    su gs :: Goals
    gs = case (Goal -> Maybe Goal) -> [Goal] -> Maybe [Goal]
    forall (t :: * -> *) a.
    Traversable t =>
    (a -> Maybe a) -> t a -> Maybe (t a)
    anyJust Goal -> Maybe Goal
    apG (Goals -> [Goal]
    fromGoals Goals
    gs) of
                        Nothing  -> Goals
    gs
                        Just gs1 :: [Goal]
    gs1 -> [Goal] -> Goals
    goalsFromList ((Goal -> [Goal]) -> [Goal] -> [Goal]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Goal -> [Goal]
    norm [Goal]
    gs1)
        where
        norm :: Goal -> [Goal]
    norm g :: Goal
    g = [ Goal
    g { goal :: Prop
    goal = Prop
    p } | Prop
    p <- Prop -> [Prop]
    pSplitAnd (Goal -> Prop
    goal Goal
    g) ]
        apG :: Goal -> Maybe Goal
    apG g :: Goal
    g  = Goal -> Prop -> Goal
    mk Goal
    g (Prop -> Goal) -> Maybe Prop -> Maybe Goal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Subst -> Prop -> Maybe Prop
    apSubstMaybe Subst
    su (Goal -> Prop
    goal Goal
    g)
        mk :: Goal -> Prop -> Goal
    mk g :: Goal
    g p :: Prop
    p = Goal
    g { goal :: Prop
    goal = Prop
    p }

    instance TVars Goal where
      apSubst :: Subst -> Goal -> Goal
    apSubst su :: Subst
    su g :: Goal
    g = Goal :: ConstraintSource -> Range -> Prop -> Goal
    Goal { goalSource :: ConstraintSource
    goalSource = Subst -> ConstraintSource -> ConstraintSource
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Goal -> ConstraintSource
    goalSource Goal
    g)
                          , goalRange :: Range
    goalRange  = Goal -> Range
    goalRange Goal
    g
                          , goal :: Prop
    goal       = Subst -> Prop -> Prop
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (Goal -> Prop
    goal Goal
    g)
                          }

    instance TVars HasGoal where
      apSubst :: Subst -> HasGoal -> HasGoal
    apSubst su :: Subst
    su h :: HasGoal
    h = HasGoal
    h { hasGoal :: Goal
    hasGoal = Subst -> Goal -> Goal
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (HasGoal -> Goal
    hasGoal HasGoal
    h) }

    instance TVars DelayedCt where
      apSubst :: Subst -> DelayedCt -> DelayedCt
    apSubst su :: Subst
    su g :: DelayedCt
    g
        | Set TVar -> Bool
    forall a. Set a -> Bool
    Set.null Set TVar
    captured =
           DelayedCt :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> DelayedCt
    DelayedCt { dctSource :: Maybe Name
    dctSource = DelayedCt -> Maybe Name
    dctSource DelayedCt
    g
                     , dctForall :: [TParam]
    dctForall = DelayedCt -> [TParam]
    dctForall DelayedCt
    g
                     , dctAsmps :: [Prop]
    dctAsmps  = Subst -> [Prop] -> [Prop]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (DelayedCt -> [Prop]
    dctAsmps DelayedCt
    g)
                     , dctGoals :: [Goal]
    dctGoals  = Subst -> [Goal] -> [Goal]
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su (DelayedCt -> [Goal]
    dctGoals DelayedCt
    g)
                     }

        | Bool
    otherwise = FilePath -> [FilePath] -> DelayedCt
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "Cryptol.TypeCheck.Subst.apSubst (DelayedCt)"
                        [ "Captured quantified variables:"
                        , "Substitution: " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Subst -> FilePath
    forall a. Show a => a -> FilePath
    show Subst
    su
                        , "Variables:    " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Set TVar -> FilePath
    forall a. Show a => a -> FilePath
    show Set TVar
    captured
                        , "Constraint:   " FilePath -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ DelayedCt -> FilePath
    forall a. Show a => a -> FilePath
    show DelayedCt
    g
                        ]

        where
        captured :: Set TVar
    captured = [TVar] -> Set TVar
    forall a. Ord a => [a] -> Set a
    Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar (DelayedCt -> [TParam]
    dctForall DelayedCt
    g))
                   Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.intersection`
                   Set TVar
    subVars
        subVars :: Set TVar
    subVars = [Set TVar] -> Set TVar
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions
                    ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
    forall a b. (a -> b) -> a -> b
    $ (TVar -> Set TVar) -> [TVar] -> [Set TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Prop -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (Maybe Prop -> Set TVar)
    -> (TVar -> Maybe Prop) -> TVar -> Set TVar
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Subst -> TVar -> Maybe Prop
    applySubstToVar Subst
    su)
                    ([TVar] -> [Set TVar]) -> [TVar] -> [Set TVar]
    forall a b. (a -> b) -> a -> b
    $ Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList Set TVar
    used
        used :: Set TVar
    used = ([Prop], [Prop]) -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs (DelayedCt -> [Prop]
    dctAsmps DelayedCt
    g, (Goal -> Prop) -> [Goal] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> Prop
    goal (DelayedCt -> [Goal]
    dctGoals DelayedCt
    g)) Set TVar -> Set TVar -> Set TVar
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference`
                    [TVar] -> Set TVar
    forall a. Ord a => [a] -> Set a
    Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> TVar
    tpVar (DelayedCt -> [TParam]
    dctForall DelayedCt
    g))

    -- | For use in error messages
    cppKind :: Kind -> Doc
    cppKind :: Kind -> Doc
    cppKind ki :: Kind
    ki =
      case Kind
    ki of
        KNum  -> FilePath -> Doc
    text "a numeric type"
        KType -> FilePath -> Doc
    text "a value type"
        KProp -> FilePath -> Doc
    text "a constraint"
        _     -> Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    ki

    addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter :: NameMap -> t -> Doc -> Doc
    addTVarsDescsAfter nm :: NameMap
    nm t :: t
    t d :: Doc
    d
      | Set TVar -> Bool
    forall a. Set a -> Bool
    Set.null Set TVar
    vs = Doc
    d
      | Bool
    otherwise   = Doc
    d Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "where" Doc -> Doc -> Doc
    $$ [Doc] -> Doc
    vcat ((TVar -> Doc) -> [TVar] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TVar -> Doc
    desc (Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList Set TVar
    vs))
      where
      vs :: Set TVar
    vs     = t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs t
    t
      desc :: TVar -> Doc
    desc v :: TVar
    v = NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm TVar
    v Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "is" Doc -> Doc -> Doc
    <+> TVarInfo -> Doc
    forall a. PP a => a -> Doc
    pp (TVar -> TVarInfo
    tvInfo TVar
    v)

    addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
    addTVarsDescsBefore :: NameMap -> t -> Doc -> Doc
    addTVarsDescsBefore nm :: NameMap
    nm t :: t
    t d :: Doc
    d = Doc
    frontMsg Doc -> Doc -> Doc
    $$ Doc
    d Doc -> Doc -> Doc
    $$ Doc
    backMsg
      where
      (vs1 :: Set TVar
    vs1,vs2 :: Set TVar
    vs2)  = (TVar -> Bool) -> Set TVar -> (Set TVar, Set TVar)
    forall a. (a -> Bool) -> Set a -> (Set a, Set a)
    Set.partition TVar -> Bool
    isFreeTV (t -> Set TVar
    forall t. FVS t => t -> Set TVar
    fvs t
    t)

      frontMsg :: Doc
    frontMsg | Set TVar -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set TVar
    vs1  = Doc
    empty
               | Bool
    otherwise = "Failed to infer the following types:"
                             Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((TVar -> Doc) -> [TVar] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TVar -> Doc
    desc1 (Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList Set TVar
    vs1)))
      desc1 :: TVar -> Doc
    desc1 v :: TVar
    v    = "•" Doc -> Doc -> Doc
    <+> NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm TVar
    v Doc -> Doc -> Doc
    <.> Doc
    comma Doc -> Doc -> Doc
    <+> TVarInfo -> Doc
    forall a. PP a => a -> Doc
    pp (TVar -> TVarInfo
    tvInfo TVar
    v)

      backMsg :: Doc
    backMsg  | Set TVar -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set TVar
    vs2  = Doc
    empty
               | Bool
    otherwise = "where"
                             Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((TVar -> Doc) -> [TVar] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TVar -> Doc
    desc2 (Set TVar -> [TVar]
    forall a. Set a -> [a]
    Set.toList Set TVar
    vs2)))
      desc2 :: TVar -> Doc
    desc2 v :: TVar
    v    = NameMap -> TVar -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    nm TVar
    v Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "is" Doc -> Doc -> Doc
    <+> TVarInfo -> Doc
    forall a. PP a => a -> Doc
    pp (TVar -> TVarInfo
    tvInfo TVar
    v)

    instance PP ConstraintSource where
      ppPrec :: Int -> ConstraintSource -> Doc
    ppPrec _ src :: ConstraintSource
    src =
        case ConstraintSource
    src of
          CtComprehension -> "list comprehension"
          CtSplitPat      -> "split (#) pattern"
          CtTypeSig       -> "type signature"
          CtInst e :: Expr
    e        -> "use of" Doc -> Doc -> Doc
    <+> Expr -> Doc
    ppUse Expr
    e
          CtSelector      -> "use of selector"
          CtExactType     -> "matching types"
          CtEnumeration   -> "list enumeration"
          CtDefaulting    -> "defaulting"
          CtPartialTypeFun f :: Name
    f -> "use of partial type function" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    f
          CtImprovement   -> "examination of collected goals"
          CtPattern desc :: Doc
    desc  -> "checking a pattern:" Doc -> Doc -> Doc
    <+> Doc
    desc
          CtModuleInstance n :: ModName
    n -> "module instantiation" Doc -> Doc -> Doc
    <+> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    n

    ppUse :: Expr -> Doc
    ppUse :: Expr -> Doc
    ppUse expr :: Expr
    expr =
      case Expr
    expr of
        EVar (Name -> Maybe Ident
    asPrim -> Just prim :: Ident
    prim)
          | Ident -> Text
    identText Ident
    prim Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "number"       -> "literal or demoted expression"
          | Ident -> Text
    identText Ident
    prim Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "infFrom"      -> "infinite enumeration"
          | Ident -> Text
    identText Ident
    prim Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "infFromThen"  -> "infinite enumeration (with step)"
          | Ident -> Text
    identText Ident
    prim Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "fromTo"       -> "finite enumeration"
          | Ident -> Text
    identText Ident
    prim Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == "fromThenTo"   -> "finite enumeration"
        _                                    -> "expression" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. PP a => a -> Doc
    pp Expr
    expr

    instance PP (WithNames Goal) where
      ppPrec :: Int -> WithNames Goal -> Doc
    ppPrec _ (WithNames g :: Goal
    g names :: NameMap
    names) =
          (NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    names (Goal -> Prop
    goal Goal
    g)) Doc -> Doc -> Doc
    $$
                   Int -> Doc -> Doc
    nest 2 (FilePath -> Doc
    text "arising from" Doc -> Doc -> Doc
    $$
                           ConstraintSource -> Doc
    forall a. PP a => a -> Doc
    pp (Goal -> ConstraintSource
    goalSource Goal
    g)   Doc -> Doc -> Doc
    $$
                           FilePath -> Doc
    text "at" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp (Goal -> Range
    goalRange Goal
    g))

    instance PP (WithNames DelayedCt) where
      ppPrec :: Int -> WithNames DelayedCt -> Doc
    ppPrec _ (WithNames d :: DelayedCt
    d names :: NameMap
    names) =
        Doc
    sig Doc -> Doc -> Doc
    $$ "we need to show that" Doc -> Doc -> Doc
    $$
        Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat [ Doc
    vars, Doc
    asmps, "the following constraints hold:"
                     , Int -> Doc -> Doc
    nest 2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    vcat
                              ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> [Doc]
    bullets
                              ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Goal -> Doc) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Goal -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1)
                              ([Goal] -> [Doc]) -> [Goal] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ DelayedCt -> [Goal]
    dctGoals DelayedCt
    d ])
        where
        bullets :: [Doc] -> [Doc]
    bullets xs :: [Doc]
    xs = [ "•" Doc -> Doc -> Doc
    <+> Doc
    x | Doc
    x <- [Doc]
    xs ]

        sig :: Doc
    sig = case Maybe Name
    name of
                Just n :: Name
    n -> "in the definition of" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n) Doc -> Doc -> Doc
    <.>
                          Doc
    comma Doc -> Doc -> Doc
    <+> "at" Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp (Name -> Range
    nameLoc Name
    n) Doc -> Doc -> Doc
    <.> Doc
    comma
                Nothing -> "when checking the module's parameters,"

        name :: Maybe Name
    name  = DelayedCt -> Maybe Name
    dctSource DelayedCt
    d
        vars :: Doc
    vars = case DelayedCt -> [TParam]
    dctForall DelayedCt
    d of
                 [] -> Doc
    empty
                 xs :: [TParam]
    xs -> "for any type" Doc -> Doc -> Doc
    <+>
                          [Doc] -> Doc
    fsep (Doc -> [Doc] -> [Doc]
    punctuate Doc
    comma ((TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> TParam -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1 ) [TParam]
    xs))
        asmps :: Doc
    asmps = case DelayedCt -> [Prop]
    dctAsmps DelayedCt
    d of
                  [] -> Doc
    empty
                  xs :: [Prop]
    xs -> "assuming" Doc -> Doc -> Doc
    $$
                        Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ([Doc] -> [Doc]
    bullets ((Prop -> Doc) -> [Prop] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameMap -> Prop -> Doc
    forall a. PP (WithNames a) => NameMap -> a -> Doc
    ppWithNames NameMap
    ns1) [Prop]
    xs)))

        ns1 :: NameMap
    ns1 = [TParam] -> NameMap -> NameMap
    addTNames (DelayedCt -> [TParam]
    dctForall DelayedCt
    d) NameMap
    names