{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998


The @Inst@ type: dictionaries or method instances
-}

{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}

module Inst (
       deeplySkolemise,
       topInstantiate, topInstantiateInferred, deeplyInstantiate,
       instCall, instDFunType, instStupidTheta, instTyVarsWith,
       newWanted, newWanteds,

       tcInstTyBinders, tcInstTyBinder,

       newOverloadedLit, mkOverLit,

       newClsInst,
       tcGetInsts, tcGetInstEnvs, getOverlapFlag,
       tcExtendLocalInstEnv,
       instCallConstraints, newMethodFromName,
       tcSyntaxName,

       -- Simple functions over evidence variables
       tyCoVarsOfWC,
       tyCoVarsOfCt, tyCoVarsOfCts,
    ) where

#include "HsVersions.h"

import GhcPrelude

import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
import {-# SOURCE #-}   TcUnify( unifyType, unifyKind )

import BasicTypes ( IntegralLit(..), SourceText(..) )
import FastString
import HsSyn
import TcHsSyn
import TcRnMonad
import TcEnv
import TcEvidence
import InstEnv
import TysWiredIn  ( heqDataCon, eqDataCon )
import CoreSyn     ( isOrphan )
import FunDeps
import TcMType
import Type
import TyCoRep
import TcType
import HscTypes
import Class( Class )
import MkId( mkDictFunId )
import CoreSyn( Expr(..) )  -- For the Coercion constructor
import Id
import Name
import Var      ( EvVar, mkTyVar, tyVarName, VarBndr(..) )
import DataCon
import VarEnv
import PrelNames
import SrcLoc
import DynFlags
import Util
import Outputable
import qualified GHC.LanguageExtensions as LangExt

import Control.Monad( unless )

{-
************************************************************************
*                                                                      *
                Creating and emittind constraints
*                                                                      *
************************************************************************
-}

newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr GhcTcId)
-- Used when Name is the wired-in name for a wired-in class method,
-- so the caller knows its type for sure, which should be of form
--    forall a. C a => <blah>
-- newMethodFromName is supposed to instantiate just the outer
-- type variable and constraint

newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr GhcTcId)
newMethodFromName origin :: CtOrigin
origin name :: Name
name inst_ty :: TcRhoType
inst_ty
  = do { Id
id <- Name -> TcM Id
tcLookupId Name
name
              -- Use tcLookupId not tcLookupGlobalId; the method is almost
              -- always a class op, but with -XRebindableSyntax GHC is
              -- meant to find whatever thing is in scope, and that may
              -- be an ordinary function.

       ; let ty :: TcRhoType
ty = HasDebugCallStack => TcRhoType -> TcRhoType -> TcRhoType
TcRhoType -> TcRhoType -> TcRhoType
piResultTy (Id -> TcRhoType
idType Id
id) TcRhoType
inst_ty
             (theta :: ThetaType
theta, _caller_knows_this :: TcRhoType
_caller_knows_this) = TcRhoType -> (ThetaType, TcRhoType)
tcSplitPhiTy TcRhoType
ty
       ; HsWrapper
wrap <- ASSERT( not (isForAllTy ty) && isSingleton theta )
                 CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
origin [TcRhoType
inst_ty] ThetaType
theta

       ; HsExpr GhcTcId -> TcM (HsExpr GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTcId -> HsExpr GhcTcId
forall (id :: Pass).
HsWrapper -> HsExpr (GhcPass id) -> HsExpr (GhcPass id)
mkHsWrap HsWrapper
wrap (XVar GhcTcId -> Located (IdP GhcTcId) -> HsExpr GhcTcId
forall p. XVar p -> Located (IdP p) -> HsExpr p
HsVar XVar GhcTcId
NoExt
noExt (SrcSpanLess (Located Id) -> Located Id
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc SrcSpanLess (Located Id)
Id
id))) }

{-
************************************************************************
*                                                                      *
        Deep instantiation and skolemisation
*                                                                      *
************************************************************************

Note [Deep skolemisation]
~~~~~~~~~~~~~~~~~~~~~~~~~
deeplySkolemise decomposes and skolemises a type, returning a type
with all its arrows visible (ie not buried under foralls)

Examples:

  deeplySkolemise (Int -> forall a. Ord a => blah)
    =  ( wp, [a], [d:Ord a], Int -> blah )
    where wp = \x:Int. /\a. \(d:Ord a). <hole> x

  deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
    where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x

In general,
  if      deeplySkolemise ty = (wrap, tvs, evs, rho)
    and   e :: rho
  then    wrap e :: ty
    and   'wrap' binds tvs, evs

ToDo: this eta-abstraction plays fast and loose with termination,
      because it can introduce extra lambdas.  Maybe add a `seq` to
      fix this
-}

deeplySkolemise :: TcSigmaType
                -> TcM ( HsWrapper
                       , [(Name,TyVar)]     -- All skolemised variables
                       , [EvVar]            -- All "given"s
                       , TcRhoType )

deeplySkolemise :: TcRhoType -> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
deeplySkolemise ty :: TcRhoType
ty
  = TCvSubst
-> TcRhoType -> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
go TCvSubst
init_subst TcRhoType
ty
  where
    init_subst :: TCvSubst
init_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (TcRhoType -> VarSet
tyCoVarsOfType TcRhoType
ty))

    go :: TCvSubst
-> TcRhoType -> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
go subst :: TCvSubst
subst ty :: TcRhoType
ty
      | Just (arg_tys :: ThetaType
arg_tys, tvs :: [Id]
tvs, theta :: ThetaType
theta, ty' :: TcRhoType
ty') <- TcRhoType -> Maybe (ThetaType, [Id], ThetaType, TcRhoType)
tcDeepSplitSigmaTy_maybe TcRhoType
ty
      = do { let arg_tys' :: ThetaType
arg_tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
arg_tys
           ; [Id]
ids1           <- FastString -> ThetaType -> TcRnIf TcGblEnv TcLclEnv [Id]
forall gbl lcl. FastString -> ThetaType -> TcRnIf gbl lcl [Id]
newSysLocalIds (String -> FastString
fsLit "dk") ThetaType
arg_tys'
           ; (subst' :: TCvSubst
subst', tvs1 :: [Id]
tvs1) <- TCvSubst -> [Id] -> TcM (TCvSubst, [Id])
tcInstSkolTyVarsX TCvSubst
subst [Id]
tvs
           ; [Id]
ev_vars1       <- ThetaType -> TcRnIf TcGblEnv TcLclEnv [Id]
newEvVars (HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst' ThetaType
theta)
           ; (wrap :: HsWrapper
wrap, tvs_prs2 :: [(Name, Id)]
tvs_prs2, ev_vars2 :: [Id]
ev_vars2, rho :: TcRhoType
rho) <- TCvSubst
-> TcRhoType -> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
go TCvSubst
subst' TcRhoType
ty'
           ; let tv_prs1 :: [(Name, Id)]
tv_prs1 = (Id -> Name) -> [Id] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Name
tyVarName [Id]
tvs [Name] -> [Id] -> [(Name, Id)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Id]
tvs1
           ; (HsWrapper, [(Name, Id)], [Id], TcRhoType)
-> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Id] -> HsWrapper
mkWpLams [Id]
ids1
                      HsWrapper -> HsWrapper -> HsWrapper
<.> [Id] -> HsWrapper
mkWpTyLams [Id]
tvs1
                      HsWrapper -> HsWrapper -> HsWrapper
<.> [Id] -> HsWrapper
mkWpLams [Id]
ev_vars1
                      HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap
                      HsWrapper -> HsWrapper -> HsWrapper
<.> [Id] -> HsWrapper
mkWpEvVarApps [Id]
ids1
                    , [(Name, Id)]
tv_prs1  [(Name, Id)] -> [(Name, Id)] -> [(Name, Id)]
forall a. [a] -> [a] -> [a]
++ [(Name, Id)]
tvs_prs2
                    , [Id]
ev_vars1 [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
ev_vars2
                    , ThetaType -> TcRhoType -> TcRhoType
mkFunTys ThetaType
arg_tys' TcRhoType
rho ) }

      | Bool
otherwise
      = (HsWrapper, [(Name, Id)], [Id], TcRhoType)
-> TcM (HsWrapper, [(Name, Id)], [Id], TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], [], HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst TcRhoType
ty)
        -- substTy is a quick no-op on an empty substitution

-- | Instantiate all outer type variables
-- and any context. Never looks through arrows.
topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- if    topInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho  (that is, wrap :: ty "->" rho)
topInstantiate :: CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
topInstantiate = Bool -> CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
top_instantiate Bool
True

-- | Instantiate all outer 'Inferred' binders
-- and any context. Never looks through arrows or specified type variables.
-- Used for visible type application.
topInstantiateInferred :: CtOrigin -> TcSigmaType
                       -> TcM (HsWrapper, TcSigmaType)
-- if    topInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho
topInstantiateInferred :: CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
topInstantiateInferred = Bool -> CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
top_instantiate Bool
False

top_instantiate :: Bool   -- True  <=> instantiate *all* variables
                          -- False <=> instantiate only the inferred ones
                -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
top_instantiate :: Bool -> CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
top_instantiate inst_all :: Bool
inst_all orig :: CtOrigin
orig ty :: TcRhoType
ty
  | Bool -> Bool
not ([TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
binders Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
  = do { let (inst_bndrs :: [TyVarBinder]
inst_bndrs, leave_bndrs :: [TyVarBinder]
leave_bndrs) = (TyVarBinder -> Bool)
-> [TyVarBinder] -> ([TyVarBinder], [TyVarBinder])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span TyVarBinder -> Bool
forall tv. VarBndr tv ArgFlag -> Bool
should_inst [TyVarBinder]
binders
             (inst_theta :: ThetaType
inst_theta, leave_theta :: ThetaType
leave_theta)
               | [TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
leave_bndrs = (ThetaType
theta, [])
               | Bool
otherwise        = ([], ThetaType
theta)
             in_scope :: InScopeSet
in_scope    = VarSet -> InScopeSet
mkInScopeSet (TcRhoType -> VarSet
tyCoVarsOfType TcRhoType
ty)
             empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope
             inst_tvs :: [Id]
inst_tvs    = [TyVarBinder] -> [Id]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
inst_bndrs
       ; (subst :: TCvSubst
subst, inst_tvs' :: [Id]
inst_tvs') <- (TCvSubst -> Id -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, Id))
-> TCvSubst -> [Id] -> TcM (TCvSubst, [Id])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM TCvSubst -> Id -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, Id)
newMetaTyVarX TCvSubst
empty_subst [Id]
inst_tvs
       ; let inst_theta' :: ThetaType
inst_theta' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst ThetaType
inst_theta
             sigma' :: TcRhoType
sigma'      = HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst ([TyVarBinder] -> TcRhoType -> TcRhoType
mkForAllTys [TyVarBinder]
leave_bndrs (TcRhoType -> TcRhoType) -> TcRhoType -> TcRhoType
forall a b. (a -> b) -> a -> b
$
                                          ThetaType -> TcRhoType -> TcRhoType
mkFunTys ThetaType
leave_theta TcRhoType
rho)
             inst_tv_tys' :: ThetaType
inst_tv_tys' = [Id] -> ThetaType
mkTyVarTys [Id]
inst_tvs'

       ; HsWrapper
wrap1 <- CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
orig ThetaType
inst_tv_tys' ThetaType
inst_theta'
       ; String -> SDoc -> TcRn ()
traceTc "Instantiating"
                 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "all tyvars?" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
inst_all
                       , String -> SDoc
text "origin" SDoc -> SDoc -> SDoc
<+> CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig
                       , String -> SDoc
text "type" SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
debugPprType TcRhoType
ty
                       , String -> SDoc
text "theta" SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
theta
                       , String -> SDoc
text "leave_bndrs" SDoc -> SDoc -> SDoc
<+> [TyVarBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVarBinder]
leave_bndrs
                       , String -> SDoc
text "with" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((TcRhoType -> SDoc) -> ThetaType -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map TcRhoType -> SDoc
debugPprType ThetaType
inst_tv_tys')
                       , String -> SDoc
text "theta:" SDoc -> SDoc -> SDoc
<+>  ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_theta' ])

       ; (wrap2 :: HsWrapper
wrap2, rho2 :: TcRhoType
rho2) <-
           if [TyVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBinder]
leave_bndrs

         -- account for types like forall a. Num a => forall b. Ord b => ...
           then Bool -> CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
top_instantiate Bool
inst_all CtOrigin
orig TcRhoType
sigma'

         -- but don't loop if there were any un-inst'able tyvars
           else (HsWrapper, TcRhoType) -> TcM (HsWrapper, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcRhoType
sigma')

       ; (HsWrapper, TcRhoType) -> TcM (HsWrapper, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1, TcRhoType
rho2) }

  | Bool
otherwise = (HsWrapper, TcRhoType) -> TcM (HsWrapper, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcRhoType
ty)
  where
    (binders :: [TyVarBinder]
binders, phi :: TcRhoType
phi) = TcRhoType -> ([TyVarBinder], TcRhoType)
tcSplitForAllVarBndrs TcRhoType
ty
    (theta :: ThetaType
theta, rho :: TcRhoType
rho)   = TcRhoType -> (ThetaType, TcRhoType)
tcSplitPhiTy TcRhoType
phi

    should_inst :: VarBndr tv ArgFlag -> Bool
should_inst bndr :: VarBndr tv ArgFlag
bndr
      | Bool
inst_all  = Bool
True
      | Bool
otherwise = VarBndr tv ArgFlag -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag VarBndr tv ArgFlag
bndr ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Inferred

deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
--   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
-- In general if
-- if    deeplyInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho
-- That is, wrap :: ty ~> rho
--
-- If you don't need the HsWrapper returned from this function, consider
-- using tcSplitNestedSigmaTys in TcType, which is a pure alternative that
-- only computes the returned TcRhoType.

deeplyInstantiate :: CtOrigin -> TcRhoType -> TcM (HsWrapper, TcRhoType)
deeplyInstantiate orig :: CtOrigin
orig ty :: TcRhoType
ty =
  CtOrigin -> TCvSubst -> TcRhoType -> TcM (HsWrapper, TcRhoType)
deeply_instantiate CtOrigin
orig
                     (InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (TcRhoType -> VarSet
tyCoVarsOfType TcRhoType
ty)))
                     TcRhoType
ty

deeply_instantiate :: CtOrigin
                   -> TCvSubst
                   -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- Internal function to deeply instantiate that builds on an existing subst.
-- It extends the input substitution and applies the final subtitution to
-- the types on return.  See #12549.

deeply_instantiate :: CtOrigin -> TCvSubst -> TcRhoType -> TcM (HsWrapper, TcRhoType)
deeply_instantiate orig :: CtOrigin
orig subst :: TCvSubst
subst ty :: TcRhoType
ty
  | Just (arg_tys :: ThetaType
arg_tys, tvs :: [Id]
tvs, theta :: ThetaType
theta, rho :: TcRhoType
rho) <- TcRhoType -> Maybe (ThetaType, [Id], ThetaType, TcRhoType)
tcDeepSplitSigmaTy_maybe TcRhoType
ty
  = do { (subst' :: TCvSubst
subst', tvs' :: [Id]
tvs') <- TCvSubst -> [Id] -> TcM (TCvSubst, [Id])
newMetaTyVarsX TCvSubst
subst [Id]
tvs
       ; let arg_tys' :: ThetaType
arg_tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys   TCvSubst
subst' ThetaType
arg_tys
             theta' :: ThetaType
theta'   = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst' ThetaType
theta
       ; [Id]
ids1  <- FastString -> ThetaType -> TcRnIf TcGblEnv TcLclEnv [Id]
forall gbl lcl. FastString -> ThetaType -> TcRnIf gbl lcl [Id]
newSysLocalIds (String -> FastString
fsLit "di") ThetaType
arg_tys'
       ; HsWrapper
wrap1 <- CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall CtOrigin
orig ([Id] -> ThetaType
mkTyVarTys [Id]
tvs') ThetaType
theta'
       ; String -> SDoc -> TcRn ()
traceTc "Instantiating (deeply)" ([SDoc] -> SDoc
vcat [ String -> SDoc
text "origin" SDoc -> SDoc -> SDoc
<+> CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig
                                                , String -> SDoc
text "type" SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcRhoType
ty
                                                , String -> SDoc
text "with" SDoc -> SDoc -> SDoc
<+> [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
tvs'
                                                , String -> SDoc
text "args:" SDoc -> SDoc -> SDoc
<+> [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
ids1
                                                , String -> SDoc
text "theta:" SDoc -> SDoc -> SDoc
<+>  ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
theta'
                                                , String -> SDoc
text "subst:" SDoc -> SDoc -> SDoc
<+> TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr TCvSubst
subst'])
       ; (wrap2 :: HsWrapper
wrap2, rho2 :: TcRhoType
rho2) <- CtOrigin -> TCvSubst -> TcRhoType -> TcM (HsWrapper, TcRhoType)
deeply_instantiate CtOrigin
orig TCvSubst
subst' TcRhoType
rho
       ; (HsWrapper, TcRhoType) -> TcM (HsWrapper, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> HsWrapper
mkWpLams [Id]
ids1
                    HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap2
                    HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1
                    HsWrapper -> HsWrapper -> HsWrapper
<.> [Id] -> HsWrapper
mkWpEvVarApps [Id]
ids1,
                 ThetaType -> TcRhoType -> TcRhoType
mkFunTys ThetaType
arg_tys' TcRhoType
rho2) }

  | Bool
otherwise
  = do { let ty' :: TcRhoType
ty' = HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst TcRhoType
ty
       ; String -> SDoc -> TcRn ()
traceTc "deeply_instantiate final subst"
                 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "origin:"   SDoc -> SDoc -> SDoc
<+> CtOrigin -> SDoc
pprCtOrigin CtOrigin
orig
                       , String -> SDoc
text "type:"     SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcRhoType
ty
                       , String -> SDoc
text "new type:" SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcRhoType
ty'
                       , String -> SDoc
text "subst:"    SDoc -> SDoc -> SDoc
<+> TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr TCvSubst
subst ])
      ; (HsWrapper, TcRhoType) -> TcM (HsWrapper, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcRhoType
ty') }


instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
-- Use this when you want to instantiate (forall a b c. ty) with
-- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
-- not yet match (perhaps because there are unsolved constraints; Trac #14154)
-- If they don't match, emit a kind-equality to promise that they will
-- eventually do so, and thus make a kind-homongeneous substitution.
instTyVarsWith :: CtOrigin -> [Id] -> ThetaType -> TcM TCvSubst
instTyVarsWith orig :: CtOrigin
orig tvs :: [Id]
tvs tys :: ThetaType
tys
  = TCvSubst -> [Id] -> ThetaType -> TcM TCvSubst
go TCvSubst
empty_subst [Id]
tvs ThetaType
tys
  where
    empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (ThetaType -> VarSet
tyCoVarsOfTypes ThetaType
tys))

    go :: TCvSubst -> [Id] -> ThetaType -> TcM TCvSubst
go subst :: TCvSubst
subst [] []
      = TCvSubst -> TcM TCvSubst
forall (m :: * -> *) a. Monad m => a -> m a
return TCvSubst
subst
    go subst :: TCvSubst
subst (tv :: Id
tv:tvs :: [Id]
tvs) (ty :: TcRhoType
ty:tys :: ThetaType
tys)
      | TcRhoType
tv_kind HasDebugCallStack => TcRhoType -> TcRhoType -> Bool
TcRhoType -> TcRhoType -> Bool
`tcEqType` TcRhoType
ty_kind
      = TCvSubst -> [Id] -> ThetaType -> TcM TCvSubst
go (TCvSubst -> Id -> TcRhoType -> TCvSubst
extendTCvSubst TCvSubst
subst Id
tv TcRhoType
ty) [Id]
tvs ThetaType
tys
      | Bool
otherwise
      = do { Coercion
co <- CtOrigin
-> TypeOrKind -> Role -> TcRhoType -> TcRhoType -> TcM Coercion
emitWantedEq CtOrigin
orig TypeOrKind
KindLevel Role
Nominal TcRhoType
ty_kind TcRhoType
tv_kind
           ; TCvSubst -> [Id] -> ThetaType -> TcM TCvSubst
go (TCvSubst -> Id -> TcRhoType -> TCvSubst
extendTCvSubst TCvSubst
subst Id
tv (TcRhoType
ty TcRhoType -> Coercion -> TcRhoType
`mkCastTy` Coercion
co)) [Id]
tvs ThetaType
tys }
      where
        tv_kind :: TcRhoType
tv_kind = HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst (Id -> TcRhoType
tyVarKind Id
tv)
        ty_kind :: TcRhoType
ty_kind = HasDebugCallStack => TcRhoType -> TcRhoType
TcRhoType -> TcRhoType
tcTypeKind TcRhoType
ty

    go _ _ _ = String -> SDoc -> TcM TCvSubst
forall a. HasCallStack => String -> SDoc -> a
pprPanic "instTysWith" ([Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
tvs SDoc -> SDoc -> SDoc
$$ ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
tys)

{-
************************************************************************
*                                                                      *
            Instantiating a call
*                                                                      *
************************************************************************

Note [Handling boxed equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The solver deals entirely in terms of unboxed (primitive) equality.
There should never be a boxed Wanted equality. Ever. But, what if
we are calling `foo :: forall a. (F a ~ Bool) => ...`? That equality
is boxed, so naive treatment here would emit a boxed Wanted equality.

So we simply check for this case and make the right boxing of evidence.

-}

----------------
instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
-- Instantiate the constraints of a call
--      (instCall o tys theta)
-- (a) Makes fresh dictionaries as necessary for the constraints (theta)
-- (b) Throws these dictionaries into the LIE
-- (c) Returns an HsWrapper ([.] tys dicts)

instCall :: CtOrigin
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCall orig :: CtOrigin
orig tys :: ThetaType
tys theta :: ThetaType
theta
  = do  { HsWrapper
dict_app <- CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints CtOrigin
orig ThetaType
theta
        ; HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
dict_app HsWrapper -> HsWrapper -> HsWrapper
<.> ThetaType -> HsWrapper
mkWpTyApps ThetaType
tys) }

----------------
instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
-- Instantiates the TcTheta, puts all constraints thereby generated
-- into the LIE, and returns a HsWrapper to enclose the call site.

instCallConstraints :: CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints orig :: CtOrigin
orig preds :: ThetaType
preds
  | ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
preds
  = HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
idHsWrapper
  | Bool
otherwise
  = do { [EvTerm]
evs <- (TcRhoType -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm)
-> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) [EvTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcRhoType -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
go ThetaType
preds
       ; String -> SDoc -> TcRn ()
traceTc "instCallConstraints" ([EvTerm] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvTerm]
evs)
       ; HsWrapper -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return ([EvTerm] -> HsWrapper
mkWpEvApps [EvTerm]
evs) }
  where
    go :: TcPredType -> TcM EvTerm
    go :: TcRhoType -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
go pred :: TcRhoType
pred
     | Just (Nominal, ty1 :: TcRhoType
ty1, ty2 :: TcRhoType
ty2) <- TcRhoType -> Maybe (Role, TcRhoType, TcRhoType)
getEqPredTys_maybe TcRhoType
pred -- Try short-cut #1
     = do  { Coercion
co <- Maybe (HsExpr GhcRn) -> TcRhoType -> TcRhoType -> TcM Coercion
unifyType Maybe (HsExpr GhcRn)
forall a. Maybe a
Nothing TcRhoType
ty1 TcRhoType
ty2
           ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> EvTerm
evCoercion Coercion
co) }

       -- Try short-cut #2
     | Just (tc :: TyCon
tc, args :: ThetaType
args@[_, _, ty1 :: TcRhoType
ty1, ty2 :: TcRhoType
ty2]) <- HasDebugCallStack => TcRhoType -> Maybe (TyCon, ThetaType)
TcRhoType -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe TcRhoType
pred
     , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
     = do { Coercion
co <- Maybe (HsExpr GhcRn) -> TcRhoType -> TcRhoType -> TcM Coercion
unifyType Maybe (HsExpr GhcRn)
forall a. Maybe a
Nothing TcRhoType
ty1 TcRhoType
ty2
          ; EvTerm -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> ThetaType -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> Id
dataConWrapId DataCon
heqDataCon) ThetaType
args [Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
co]) }

     | Bool
otherwise
     = CtOrigin -> TcRhoType -> IOEnv (Env TcGblEnv TcLclEnv) EvTerm
emitWanted CtOrigin
orig TcRhoType
pred

instDFunType :: DFunId -> [DFunInstType]
             -> TcM ( [TcType]      -- instantiated argument types
                    , TcThetaType ) -- instantiated constraint
-- See Note [DFunInstType: instantiating types] in InstEnv
instDFunType :: Id -> [DFunInstType] -> TcM (ThetaType, ThetaType)
instDFunType dfun_id :: Id
dfun_id dfun_inst_tys :: [DFunInstType]
dfun_inst_tys
  = do { (subst :: TCvSubst
subst, inst_tys :: ThetaType
inst_tys) <- TCvSubst -> [Id] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go TCvSubst
empty_subst [Id]
dfun_tvs [DFunInstType]
dfun_inst_tys
       ; (ThetaType, ThetaType) -> TcM (ThetaType, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (ThetaType
inst_tys, HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst ThetaType
dfun_theta) }
  where
    dfun_ty :: TcRhoType
dfun_ty = Id -> TcRhoType
idType Id
dfun_id
    (dfun_tvs :: [Id]
dfun_tvs, dfun_theta :: ThetaType
dfun_theta, _) = TcRhoType -> ([Id], ThetaType, TcRhoType)
tcSplitSigmaTy TcRhoType
dfun_ty
    empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (TcRhoType -> VarSet
tyCoVarsOfType TcRhoType
dfun_ty))
                  -- With quantified constraints, the
                  -- type of a dfun may not be closed

    go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
    go :: TCvSubst -> [Id] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go subst :: TCvSubst
subst [] [] = (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, [])
    go subst :: TCvSubst
subst (tv :: Id
tv:tvs :: [Id]
tvs) (Just ty :: TcRhoType
ty : mb_tys :: [DFunInstType]
mb_tys)
      = do { (subst' :: TCvSubst
subst', tys :: ThetaType
tys) <- TCvSubst -> [Id] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go (TCvSubst -> Id -> TcRhoType -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst Id
tv TcRhoType
ty)
                                 [Id]
tvs
                                 [DFunInstType]
mb_tys
           ; (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', TcRhoType
ty TcRhoType -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
: ThetaType
tys) }
    go subst :: TCvSubst
subst (tv :: Id
tv:tvs :: [Id]
tvs) (Nothing : mb_tys :: [DFunInstType]
mb_tys)
      = do { (subst' :: TCvSubst
subst', tv' :: Id
tv') <- TCvSubst -> Id -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, Id)
newMetaTyVarX TCvSubst
subst Id
tv
           ; (subst'' :: TCvSubst
subst'', tys :: ThetaType
tys) <- TCvSubst -> [Id] -> [DFunInstType] -> TcM (TCvSubst, ThetaType)
go TCvSubst
subst' [Id]
tvs [DFunInstType]
mb_tys
           ; (TCvSubst, ThetaType) -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst'', Id -> TcRhoType
mkTyVarTy Id
tv' TcRhoType -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
: ThetaType
tys) }
    go _ _ _ = String -> SDoc -> TcM (TCvSubst, ThetaType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "instDFunTypes" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
dfun_id SDoc -> SDoc -> SDoc
$$ [DFunInstType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunInstType]
dfun_inst_tys)

----------------
instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
-- Similar to instCall, but only emit the constraints in the LIE
-- Used exclusively for the 'stupid theta' of a data constructor
instStupidTheta :: CtOrigin -> ThetaType -> TcRn ()
instStupidTheta orig :: CtOrigin
orig theta :: ThetaType
theta
  = do  { HsWrapper
_co <- CtOrigin -> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) HsWrapper
instCallConstraints CtOrigin
orig ThetaType
theta -- Discard the coercion
        ; () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }

{-
************************************************************************
*                                                                      *
         Instantiating Kinds
*                                                                      *
************************************************************************

Note [Constraints handled in types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, we cannot handle constraints written in types. For example,
if we declare

  data C a where
    MkC :: Show a => a -> C a

we will not be able to use MkC in types, as we have no way of creating
a type-level Show dictionary.

However, we make an exception for equality types. Consider

  data T1 a where
    MkT1 :: T1 Bool

  data T2 a where
    MkT2 :: a ~ Bool => T2 a

MkT1 has a constrained return type, while MkT2 uses an explicit equality
constraint. These two types are often written interchangeably, with a
reasonable expectation that they mean the same thing. For this to work --
and for us to be able to promote GADTs -- we need to be able to instantiate
equality constraints in types.

One wrinkle is that the equality in MkT2 is *lifted*. But, for proper
GADT equalities, GHC produces *unlifted* constraints. (This unlifting comes
from DataCon.eqSpecPreds, which uses mkPrimEqPred.) And, perhaps a wily
user will use (~~) for a heterogeneous equality. We thus must support
all of (~), (~~), and (~#) in types. (See Note [The equality types story]
in TysPrim for a primer on these equality types.)

The get_eq_tys_maybe function recognizes these three forms of equality,
returning a suitable type formation function and the two types related
by the equality constraint. In the lifted case, it uses mkHEqBoxTy or
mkEqBoxTy, which promote the datacons of the (~~) or (~) datatype,
respectively.

One might reasonably wonder who *unpacks* these boxes once they are
made. After all, there is no type-level `case` construct. The surprising
answer is that no one ever does. Instead, if a GADT constructor is used
on the left-hand side of a type family equation, that occurrence forces
GHC to unify the types in question. For example:

  data G a where
    MkG :: G Bool

  type family F (x :: G a) :: a where
    F MkG = False

When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
unify F's implicit parameter `a` with Bool. This succeeds, making the equation

    F Bool (MkG @Bool <Bool>) = False

Note that we never need unpack the coercion. This is because type family
equations are *not* parametric in their kind variables. That is, we could have
just said

  type family H (x :: G a) :: a where
    H _ = False

The presence of False on the RHS also forces `a` to become Bool, giving us

    H Bool _ = False

The fact that any of this works stems from the lack of phase separation between
types and kinds (unlike the very present phase separation between terms and types).

Once we have the ability to pattern-match on types below top-level, this will
no longer cut it, but it seems fine for now.

-}

---------------------------
-- | Instantantiate the TyConBinders of a forall type,
--   given its decomposed form (tvs, ty)
tcInstTyBinders :: HasDebugCallStack
              => ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
              -> TcM ([TcType], TcKind)   -- ^ Instantiated bs, substituted ty
-- Takes a pair because that is what splitPiTysInvisible returns
-- See also Note [Bidirectional type checking]
tcInstTyBinders :: ([TyCoBinder], TcRhoType) -> TcM (ThetaType, TcRhoType)
tcInstTyBinders (bndrs :: [TyCoBinder]
bndrs, ty :: TcRhoType
ty)
  | [TyCoBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoBinder]
bndrs        -- It's fine for bndrs to be empty e.g.
  = (ThetaType, TcRhoType) -> TcM (ThetaType, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], TcRhoType
ty)   -- Check that (Maybe :: forall {k}. k->*),
                      --       and see the call to instTyBinders in checkExpectedKind
                      -- A user bug to be reported as such; it is not a compiler crash!

  | Bool
otherwise
  = do { (subst :: TCvSubst
subst, args :: ThetaType
args) <- (TCvSubst
 -> TyCoBinder
 -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType))
-> TCvSubst -> [TyCoBinder] -> TcM (TCvSubst, ThetaType)
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (Maybe (VarEnv TcRhoType)
-> TCvSubst
-> TyCoBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
tcInstTyBinder Maybe (VarEnv TcRhoType)
forall a. Maybe a
Nothing) TCvSubst
empty_subst [TyCoBinder]
bndrs
       ; TcRhoType
ty' <- TcRhoType -> TcM TcRhoType
zonkTcType (HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst TcRhoType
ty)
                   -- Why zonk the result? So that tcTyVar can
                   -- obey (IT6) of Note [The tcType invariant] in TcHsType
                   -- ToDo: SLPJ: I don't think this is needed
       ; (ThetaType, TcRhoType) -> TcM (ThetaType, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (ThetaType
args, TcRhoType
ty') }
  where
     empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (TcRhoType -> VarSet
tyCoVarsOfType TcRhoType
ty))

-- | Used only in *types*
tcInstTyBinder :: Maybe (VarEnv Kind)
               -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
tcInstTyBinder :: Maybe (VarEnv TcRhoType)
-> TCvSubst
-> TyCoBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
tcInstTyBinder mb_kind_info :: Maybe (VarEnv TcRhoType)
mb_kind_info subst :: TCvSubst
subst (Named (Bndr tv :: Id
tv _))
  = case Id -> DFunInstType
lookup_tv Id
tv of
      Just ki :: TcRhoType
ki -> (TCvSubst, TcRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> Id -> TcRhoType -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst Id
tv TcRhoType
ki, TcRhoType
ki)
      Nothing -> do { (subst' :: TCvSubst
subst', tv' :: Id
tv') <- TCvSubst -> Id -> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, Id)
newMetaTyVarX TCvSubst
subst Id
tv
                    ; (TCvSubst, TcRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', Id -> TcRhoType
mkTyVarTy Id
tv') }
  where
    lookup_tv :: Id -> DFunInstType
lookup_tv tv :: Id
tv = do { VarEnv TcRhoType
env <- Maybe (VarEnv TcRhoType)
mb_kind_info   -- `Maybe` monad
                      ; VarEnv TcRhoType -> Id -> DFunInstType
forall a. VarEnv a -> Id -> Maybe a
lookupVarEnv VarEnv TcRhoType
env Id
tv }


tcInstTyBinder _ subst :: TCvSubst
subst (Anon ty :: TcRhoType
ty)
     -- This is the *only* constraint currently handled in types.
  | Just (mk :: Coercion -> TcM TcRhoType
mk, k1 :: TcRhoType
k1, k2 :: TcRhoType
k2) <- TcRhoType
-> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
get_eq_tys_maybe TcRhoType
substed_ty
  = do { Coercion
co <- Maybe (HsType GhcRn) -> TcRhoType -> TcRhoType -> TcM Coercion
unifyKind Maybe (HsType GhcRn)
forall a. Maybe a
Nothing TcRhoType
k1 TcRhoType
k2
       ; TcRhoType
arg' <- Coercion -> TcM TcRhoType
mk Coercion
co
       ; (TCvSubst, TcRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, TcRhoType
arg') }

  | TcRhoType -> Bool
isPredTy TcRhoType
substed_ty
  = do { let (env :: TidyEnv
env, tidy_ty :: TcRhoType
tidy_ty) = TidyEnv -> TcRhoType -> (TidyEnv, TcRhoType)
tidyOpenType TidyEnv
emptyTidyEnv TcRhoType
substed_ty
       ; (TidyEnv, SDoc) -> TcRn ()
addErrTcM (TidyEnv
env, String -> SDoc
text "Illegal constraint in a kind:" SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcRhoType
tidy_ty)

         -- just invent a new variable so that we can continue
       ; Unique
u <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
       ; let name :: Name
name = Unique -> FastString -> Name
mkSysTvName Unique
u (String -> FastString
fsLit "dict")
       ; (TCvSubst, TcRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, Id -> TcRhoType
mkTyVarTy (Id -> TcRhoType) -> Id -> TcRhoType
forall a b. (a -> b) -> a -> b
$ Name -> TcRhoType -> Id
mkTyVar Name
name TcRhoType
substed_ty) }


  | Bool
otherwise
  = do { TcRhoType
tv_ty <- TcRhoType -> TcM TcRhoType
newFlexiTyVarTy TcRhoType
substed_ty
       ; (TCvSubst, TcRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TCvSubst, TcRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, TcRhoType
tv_ty) }

  where
    substed_ty :: TcRhoType
substed_ty = HasCallStack => TCvSubst -> TcRhoType -> TcRhoType
TCvSubst -> TcRhoType -> TcRhoType
substTy TCvSubst
subst TcRhoType
ty

      -- See Note [Constraints handled in types]
    get_eq_tys_maybe :: Type
                     -> Maybe ( Coercion -> TcM Type
                                 -- given a coercion proving t1 ~# t2, produce the
                                 -- right instantiation for the TyBinder at hand
                              , Type  -- t1
                              , Type  -- t2
                              )
    get_eq_tys_maybe :: TcRhoType
-> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
get_eq_tys_maybe ty :: TcRhoType
ty
        -- unlifted equality (~#)
      | Just (Nominal, k1 :: TcRhoType
k1, k2 :: TcRhoType
k2) <- TcRhoType -> Maybe (Role, TcRhoType, TcRhoType)
getEqPredTys_maybe TcRhoType
ty
      = (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
-> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. a -> Maybe a
Just (\co :: Coercion
co -> TcRhoType -> TcM TcRhoType
forall (m :: * -> *) a. Monad m => a -> m a
return (TcRhoType -> TcM TcRhoType) -> TcRhoType -> TcM TcRhoType
forall a b. (a -> b) -> a -> b
$ Coercion -> TcRhoType
mkCoercionTy Coercion
co, TcRhoType
k1, TcRhoType
k2)

        -- lifted heterogeneous equality (~~)
      | Just (tc :: TyCon
tc, [_, _, k1 :: TcRhoType
k1, k2 :: TcRhoType
k2]) <- HasDebugCallStack => TcRhoType -> Maybe (TyCon, ThetaType)
TcRhoType -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe TcRhoType
ty
      = if | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
             -> (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
-> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. a -> Maybe a
Just (\co :: Coercion
co -> Coercion -> TcRhoType -> TcRhoType -> TcM TcRhoType
mkHEqBoxTy Coercion
co TcRhoType
k1 TcRhoType
k2, TcRhoType
k1, TcRhoType
k2)
           | Bool
otherwise
             -> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. Maybe a
Nothing

        -- lifted homogeneous equality (~)
      | Just (tc :: TyCon
tc, [_, k1 :: TcRhoType
k1, k2 :: TcRhoType
k2]) <- HasDebugCallStack => TcRhoType -> Maybe (TyCon, ThetaType)
TcRhoType -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe TcRhoType
ty
      = if | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
             -> (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
-> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. a -> Maybe a
Just (\co :: Coercion
co -> Coercion -> TcRhoType -> TcRhoType -> TcM TcRhoType
mkEqBoxTy Coercion
co TcRhoType
k1 TcRhoType
k2, TcRhoType
k1, TcRhoType
k2)
           | Bool
otherwise
             -> Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. Maybe a
Nothing

      | Bool
otherwise
      = Maybe (Coercion -> TcM TcRhoType, TcRhoType, TcRhoType)
forall a. Maybe a
Nothing

-------------------------------
-- | This takes @a ~# b@ and returns @a ~~ b@.
mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-- monadic just for convenience with mkEqBoxTy
mkHEqBoxTy :: Coercion -> TcRhoType -> TcRhoType -> TcM TcRhoType
mkHEqBoxTy co :: Coercion
co ty1 :: TcRhoType
ty1 ty2 :: TcRhoType
ty2
  = TcRhoType -> TcM TcRhoType
forall (m :: * -> *) a. Monad m => a -> m a
return (TcRhoType -> TcM TcRhoType) -> TcRhoType -> TcM TcRhoType
forall a b. (a -> b) -> a -> b
$
    TyCon -> ThetaType -> TcRhoType
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
heqDataCon) [TcRhoType
k1, TcRhoType
k2, TcRhoType
ty1, TcRhoType
ty2, Coercion -> TcRhoType
mkCoercionTy Coercion
co]
  where k1 :: TcRhoType
k1 = HasDebugCallStack => TcRhoType -> TcRhoType
TcRhoType -> TcRhoType
tcTypeKind TcRhoType
ty1
        k2 :: TcRhoType
k2 = HasDebugCallStack => TcRhoType -> TcRhoType
TcRhoType -> TcRhoType
tcTypeKind TcRhoType
ty2

-- | This takes @a ~# b@ and returns @a ~ b@.
mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkEqBoxTy :: Coercion -> TcRhoType -> TcRhoType -> TcM TcRhoType
mkEqBoxTy co :: Coercion
co ty1 :: TcRhoType
ty1 ty2 :: TcRhoType
ty2
  = TcRhoType -> TcM TcRhoType
forall (m :: * -> *) a. Monad m => a -> m a
return (TcRhoType -> TcM TcRhoType) -> TcRhoType -> TcM TcRhoType
forall a b. (a -> b) -> a -> b
$
    TyCon -> ThetaType -> TcRhoType
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
eqDataCon) [TcRhoType
k, TcRhoType
ty1, TcRhoType
ty2, Coercion -> TcRhoType
mkCoercionTy Coercion
co]
  where k :: TcRhoType
k = HasDebugCallStack => TcRhoType -> TcRhoType
TcRhoType -> TcRhoType
tcTypeKind TcRhoType
ty1

{-
************************************************************************
*                                                                      *
                Literals
*                                                                      *
************************************************************************

-}

{-
In newOverloadedLit we convert directly to an Int or Integer if we
know that's what we want.  This may save some time, by not
temporarily generating overloaded literals, but it won't catch all
cases (the rest are caught in lookupInst).

-}

newOverloadedLit :: HsOverLit GhcRn
                 -> ExpRhoType
                 -> TcM (HsOverLit GhcTcId)
newOverloadedLit :: HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTcId)
newOverloadedLit
  lit :: HsOverLit GhcRn
lit@(OverLit { ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = XOverLit GhcRn
rebindable }) res_ty :: ExpRhoType
res_ty
  | Bool -> Bool
not Bool
XOverLit GhcRn
rebindable
    -- all built-in overloaded lits are tau-types, so we can just
    -- tauify the ExpType
  = do { TcRhoType
res_ty <- ExpRhoType -> TcM TcRhoType
expTypeToType ExpRhoType
res_ty
       ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; case DynFlags -> OverLitVal -> TcRhoType -> Maybe (HsExpr GhcTcId)
shortCutLit DynFlags
dflags OverLitVal
val TcRhoType
res_ty of
        -- Do not generate a LitInst for rebindable syntax.
        -- Reason: If we do, tcSimplify will call lookupInst, which
        --         will call tcSyntaxName, which does unification,
        --         which tcSimplify doesn't like
           Just expr :: HsExpr GhcTcId
expr -> HsOverLit GhcTcId -> TcM (HsOverLit GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsOverLit GhcRn
lit { ol_witness :: HsExpr GhcTcId
ol_witness = HsExpr GhcTcId
expr
                                    , ol_ext :: XOverLit GhcTcId
ol_ext = Bool -> TcRhoType -> OverLitTc
OverLitTc Bool
False TcRhoType
res_ty })
           Nothing   -> CtOrigin
-> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTcId)
newNonTrivialOverloadedLit CtOrigin
orig HsOverLit GhcRn
lit
                                                   (TcRhoType -> ExpRhoType
mkCheckExpType TcRhoType
res_ty) }

  | Bool
otherwise
  = CtOrigin
-> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTcId)
newNonTrivialOverloadedLit CtOrigin
orig HsOverLit GhcRn
lit ExpRhoType
res_ty
  where
    orig :: CtOrigin
orig = HsOverLit GhcRn -> CtOrigin
LiteralOrigin HsOverLit GhcRn
lit
newOverloadedLit XOverLit{} _ = String -> TcM (HsOverLit GhcTcId)
forall a. String -> a
panic "newOverloadedLit"

-- Does not handle things that 'shortCutLit' can handle. See also
-- newOverloadedLit in TcUnify
newNonTrivialOverloadedLit :: CtOrigin
                           -> HsOverLit GhcRn
                           -> ExpRhoType
                           -> TcM (HsOverLit GhcTcId)
newNonTrivialOverloadedLit :: CtOrigin
-> HsOverLit GhcRn -> ExpRhoType -> TcM (HsOverLit GhcTcId)
newNonTrivialOverloadedLit orig :: CtOrigin
orig
  lit :: HsOverLit GhcRn
lit@(OverLit { ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_witness :: forall p. HsOverLit p -> HsExpr p
ol_witness = HsVar _ (L _ meth_name :: IdP GhcRn
meth_name)
               , ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = XOverLit GhcRn
rebindable }) res_ty :: ExpRhoType
res_ty
  = do  { HsLit GhcTcId
hs_lit <- OverLitVal -> TcM (HsLit GhcTcId)
mkOverLit OverLitVal
val
        ; let lit_ty :: TcRhoType
lit_ty = HsLit GhcTcId -> TcRhoType
forall (p :: Pass). HsLit (GhcPass p) -> TcRhoType
hsLitType HsLit GhcTcId
hs_lit
        ; (_, fi' :: SyntaxExpr GhcTcId
fi') <- CtOrigin
-> SyntaxExpr GhcRn
-> [SyntaxOpType]
-> ExpRhoType
-> (ThetaType -> TcRn ())
-> TcM ((), SyntaxExpr GhcTcId)
forall a.
CtOrigin
-> SyntaxExpr GhcRn
-> [SyntaxOpType]
-> ExpRhoType
-> (ThetaType -> TcM a)
-> TcM (a, SyntaxExpr GhcTcId)
tcSyntaxOp CtOrigin
orig (Name -> SyntaxExpr GhcRn
mkRnSyntaxExpr Name
IdP GhcRn
meth_name)
                                      [TcRhoType -> SyntaxOpType
synKnownType TcRhoType
lit_ty] ExpRhoType
res_ty ((ThetaType -> TcRn ()) -> TcM ((), SyntaxExpr GhcTcId))
-> (ThetaType -> TcRn ()) -> TcM ((), SyntaxExpr GhcTcId)
forall a b. (a -> b) -> a -> b
$
                      \_ -> () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ; let L _ witness :: HsExpr GhcTcId
witness = SyntaxExpr GhcTcId
-> [GenLocated SrcSpan (HsExpr GhcTcId)]
-> GenLocated SrcSpan (HsExpr GhcTcId)
forall (id :: Pass).
SyntaxExpr (GhcPass id)
-> [LHsExpr (GhcPass id)] -> LHsExpr (GhcPass id)
nlHsSyntaxApps SyntaxExpr GhcTcId
fi' [HsLit GhcTcId -> GenLocated SrcSpan (HsExpr GhcTcId)
forall (p :: Pass). HsLit (GhcPass p) -> LHsExpr (GhcPass p)
nlHsLit HsLit GhcTcId
hs_lit]
        ; TcRhoType
res_ty <- ExpRhoType -> TcM TcRhoType
readExpType ExpRhoType
res_ty
        ; HsOverLit GhcTcId -> TcM (HsOverLit GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsOverLit GhcRn
lit { ol_witness :: HsExpr GhcTcId
ol_witness = HsExpr GhcTcId
witness
                      , ol_ext :: XOverLit GhcTcId
ol_ext = Bool -> TcRhoType -> OverLitTc
OverLitTc Bool
XOverLit GhcRn
rebindable TcRhoType
res_ty }) }
newNonTrivialOverloadedLit _ lit :: HsOverLit GhcRn
lit _
  = String -> SDoc -> TcM (HsOverLit GhcTcId)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "newNonTrivialOverloadedLit" (HsOverLit GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsOverLit GhcRn
lit)

------------
mkOverLit ::OverLitVal -> TcM (HsLit GhcTc)
mkOverLit :: OverLitVal -> TcM (HsLit GhcTcId)
mkOverLit (HsIntegral i :: IntegralLit
i)
  = do  { TcRhoType
integer_ty <- Name -> TcM TcRhoType
tcMetaTy Name
integerTyConName
        ; HsLit GhcTcId -> TcM (HsLit GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsInteger GhcTcId -> Integer -> TcRhoType -> HsLit GhcTcId
forall x. XHsInteger x -> Integer -> TcRhoType -> HsLit x
HsInteger (IntegralLit -> SourceText
il_text IntegralLit
i)
                            (IntegralLit -> Integer
il_value IntegralLit
i) TcRhoType
integer_ty) }

mkOverLit (HsFractional r :: FractionalLit
r)
  = do  { TcRhoType
rat_ty <- Name -> TcM TcRhoType
tcMetaTy Name
rationalTyConName
        ; HsLit GhcTcId -> TcM (HsLit GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsRat GhcTcId -> FractionalLit -> TcRhoType -> HsLit GhcTcId
forall x. XHsRat x -> FractionalLit -> TcRhoType -> HsLit x
HsRat XHsRat GhcTcId
NoExt
noExt FractionalLit
r TcRhoType
rat_ty) }

mkOverLit (HsIsString src :: SourceText
src s :: FastString
s) = HsLit GhcTcId -> TcM (HsLit GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (XHsString GhcTcId -> FastString -> HsLit GhcTcId
forall x. XHsString x -> FastString -> HsLit x
HsString SourceText
XHsString GhcTcId
src FastString
s)

{-
************************************************************************
*                                                                      *
                Re-mappable syntax

     Used only for arrow syntax -- find a way to nuke this
*                                                                      *
************************************************************************

Suppose we are doing the -XRebindableSyntax thing, and we encounter
a do-expression.  We have to find (>>) in the current environment, which is
done by the rename. Then we have to check that it has the same type as
Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
this:

  (>>) :: HB m n mn => m a -> n b -> mn b

So the idea is to generate a local binding for (>>), thus:

        let then72 :: forall a b. m a -> m b -> m b
            then72 = ...something involving the user's (>>)...
        in
        ...the do-expression...

Now the do-expression can proceed using then72, which has exactly
the expected type.

In fact tcSyntaxName just generates the RHS for then72, because we only
want an actual binding in the do-expression case. For literals, we can
just use the expression inline.
-}

tcSyntaxName :: CtOrigin
             -> TcType                 -- ^ Type to instantiate it at
             -> (Name, HsExpr GhcRn)   -- ^ (Standard name, user name)
             -> TcM (Name, HsExpr GhcTcId)
                                       -- ^ (Standard name, suitable expression)
-- USED ONLY FOR CmdTop (sigh) ***
-- See Note [CmdSyntaxTable] in HsExpr

tcSyntaxName :: CtOrigin
-> TcRhoType -> (Name, HsExpr GhcRn) -> TcM (Name, HsExpr GhcTcId)
tcSyntaxName orig :: CtOrigin
orig ty :: TcRhoType
ty (std_nm :: Name
std_nm, HsVar _ (L _ user_nm :: IdP GhcRn
user_nm))
  | Name
std_nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
IdP GhcRn
user_nm
  = do HsExpr GhcTcId
rhs <- CtOrigin -> Name -> TcRhoType -> TcM (HsExpr GhcTcId)
newMethodFromName CtOrigin
orig Name
std_nm TcRhoType
ty
       (Name, HsExpr GhcTcId) -> TcM (Name, HsExpr GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
std_nm, HsExpr GhcTcId
rhs)

tcSyntaxName orig :: CtOrigin
orig ty :: TcRhoType
ty (std_nm :: Name
std_nm, user_nm_expr :: HsExpr GhcRn
user_nm_expr) = do
    Id
std_id <- Name -> TcM Id
tcLookupId Name
std_nm
    let
        -- C.f. newMethodAtLoc
        ([tv :: Id
tv], _, tau :: TcRhoType
tau) = TcRhoType -> ([Id], ThetaType, TcRhoType)
tcSplitSigmaTy (Id -> TcRhoType
idType Id
std_id)
        sigma1 :: TcRhoType
sigma1         = HasCallStack => [Id] -> ThetaType -> TcRhoType -> TcRhoType
[Id] -> ThetaType -> TcRhoType -> TcRhoType
substTyWith [Id
tv] [TcRhoType
ty] TcRhoType
tau
        -- Actually, the "tau-type" might be a sigma-type in the
        -- case of locally-polymorphic methods.

    (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (Name, HsExpr GhcTcId) -> TcM (Name, HsExpr GhcTcId)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (HsExpr GhcRn
-> CtOrigin -> TcRhoType -> TidyEnv -> TcM (TidyEnv, SDoc)
syntaxNameCtxt HsExpr GhcRn
user_nm_expr CtOrigin
orig TcRhoType
sigma1) (TcM (Name, HsExpr GhcTcId) -> TcM (Name, HsExpr GhcTcId))
-> TcM (Name, HsExpr GhcTcId) -> TcM (Name, HsExpr GhcTcId)
forall a b. (a -> b) -> a -> b
$ do

        -- Check that the user-supplied thing has the
        -- same type as the standard one.
        -- Tiresome jiggling because tcCheckSigma takes a located expression
     SrcSpan
span <- TcRn SrcSpan
getSrcSpanM
     GenLocated SrcSpan (HsExpr GhcTcId)
expr <- LHsExpr GhcRn
-> TcRhoType -> TcM (GenLocated SrcSpan (HsExpr GhcTcId))
tcPolyExpr (SrcSpan -> HsExpr GhcRn -> LHsExpr GhcRn
forall l e. l -> e -> GenLocated l e
L SrcSpan
span HsExpr GhcRn
user_nm_expr) TcRhoType
sigma1
     (Name, HsExpr GhcTcId) -> TcM (Name, HsExpr GhcTcId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
std_nm, GenLocated SrcSpan (HsExpr GhcTcId)
-> SrcSpanLess (GenLocated SrcSpan (HsExpr GhcTcId))
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc GenLocated SrcSpan (HsExpr GhcTcId)
expr)

syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv
               -> TcRn (TidyEnv, SDoc)
syntaxNameCtxt :: HsExpr GhcRn
-> CtOrigin -> TcRhoType -> TidyEnv -> TcM (TidyEnv, SDoc)
syntaxNameCtxt name :: HsExpr GhcRn
name orig :: CtOrigin
orig ty :: TcRhoType
ty tidy_env :: TidyEnv
tidy_env
  = do { CtLoc
inst_loc <- CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM CtOrigin
orig (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
TypeLevel)
       ; let msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ String -> SDoc
text "When checking that" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
name)
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "(needed by a syntactic construct)"
                        , Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "has the required type:"
                                  SDoc -> SDoc -> SDoc
<+> TcRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TidyEnv -> TcRhoType -> TcRhoType
tidyType TidyEnv
tidy_env TcRhoType
ty))
                        , Int -> SDoc -> SDoc
nest 2 (CtLoc -> SDoc
pprCtLoc CtLoc
inst_loc) ]
       ; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg) }

{-
************************************************************************
*                                                                      *
                Instances
*                                                                      *
************************************************************************
-}

getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
-- Construct the OverlapFlag from the global module flags,
-- but if the overlap_mode argument is (Just m),
--     set the OverlapMode to 'm'
getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag overlap_mode :: Maybe OverlapMode
overlap_mode
  = do  { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
        ; let overlap_ok :: Bool
overlap_ok    = Extension -> DynFlags -> Bool
xopt Extension
LangExt.OverlappingInstances DynFlags
dflags
              incoherent_ok :: Bool
incoherent_ok = Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances  DynFlags
dflags
              use :: OverlapMode -> OverlapFlag
use x :: OverlapMode
x = OverlapFlag :: OverlapMode -> Bool -> OverlapFlag
OverlapFlag { isSafeOverlap :: Bool
isSafeOverlap = DynFlags -> Bool
safeLanguageOn DynFlags
dflags
                                  , overlapMode :: OverlapMode
overlapMode   = OverlapMode
x }
              default_oflag :: OverlapFlag
default_oflag | Bool
incoherent_ok = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Incoherent SourceText
NoSourceText)
                            | Bool
overlap_ok    = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
Overlaps SourceText
NoSourceText)
                            | Bool
otherwise     = OverlapMode -> OverlapFlag
use (SourceText -> OverlapMode
NoOverlap SourceText
NoSourceText)

              final_oflag :: OverlapFlag
final_oflag = OverlapFlag -> Maybe OverlapMode -> OverlapFlag
setOverlapModeMaybe OverlapFlag
default_oflag Maybe OverlapMode
overlap_mode
        ; OverlapFlag -> TcM OverlapFlag
forall (m :: * -> *) a. Monad m => a -> m a
return OverlapFlag
final_oflag }

tcGetInsts :: TcM [ClsInst]
-- Gets the local class instances.
tcGetInsts :: TcM [ClsInst]
tcGetInsts = (TcGblEnv -> [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv -> TcM [ClsInst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcGblEnv -> [ClsInst]
tcg_insts IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv

newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
           -> Class -> [Type] -> TcM ClsInst
newClsInst :: Maybe OverlapMode
-> Name -> [Id] -> ThetaType -> Class -> ThetaType -> TcM ClsInst
newClsInst overlap_mode :: Maybe OverlapMode
overlap_mode dfun_name :: Name
dfun_name tvs :: [Id]
tvs theta :: ThetaType
theta clas :: Class
clas tys :: ThetaType
tys
  = do { (subst :: TCvSubst
subst, tvs' :: [Id]
tvs') <- [Id] -> TcM (TCvSubst, [Id])
freshenTyVarBndrs [Id]
tvs
             -- Be sure to freshen those type variables,
             -- so they are sure not to appear in any lookup
       ; let tys' :: ThetaType
tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
tys

             dfun :: Id
dfun = Name -> [Id] -> ThetaType -> Class -> ThetaType -> Id
mkDictFunId Name
dfun_name [Id]
tvs ThetaType
theta Class
clas ThetaType
tys
             -- The dfun uses the original 'tvs' because
             -- (a) they don't need to be fresh
             -- (b) they may be mentioned in the ib_binds field of
             --     an InstInfo, and in TcEnv.pprInstInfoDetails it's
             --     helpful to use the same names

       ; OverlapFlag
oflag <- Maybe OverlapMode -> TcM OverlapFlag
getOverlapFlag Maybe OverlapMode
overlap_mode
       ; let inst :: ClsInst
inst = Id -> OverlapFlag -> [Id] -> Class -> ThetaType -> ClsInst
mkLocalInstance Id
dfun OverlapFlag
oflag [Id]
tvs' Class
clas ThetaType
tys'
       ; WarningFlag -> Bool -> SDoc -> TcRn ()
warnIfFlag WarningFlag
Opt_WarnOrphans
                    (IsOrphan -> Bool
isOrphan (ClsInst -> IsOrphan
is_orphan ClsInst
inst))
                    (ClsInst -> SDoc
instOrphWarn ClsInst
inst)
       ; ClsInst -> TcM ClsInst
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInst
inst }

instOrphWarn :: ClsInst -> SDoc
instOrphWarn :: ClsInst -> SDoc
instOrphWarn inst :: ClsInst
inst
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Orphan instance:") 2 (ClsInst -> SDoc
pprInstanceHdr ClsInst
inst)
    SDoc -> SDoc -> SDoc
$$ String -> SDoc
text "To avoid this"
    SDoc -> SDoc -> SDoc
$$ Int -> SDoc -> SDoc
nest 4 ([SDoc] -> SDoc
vcat [SDoc]
possibilities)
  where
    possibilities :: [SDoc]
possibilities =
      String -> SDoc
text "move the instance declaration to the module of the class or of the type, or" SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
:
      String -> SDoc
text "wrap the type with a newtype and declare the instance on the new type." SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
:
      []

tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
  -- Add new locally-defined instances
tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
tcExtendLocalInstEnv dfuns :: [ClsInst]
dfuns thing_inside :: TcM a
thing_inside
 = do { [ClsInst] -> TcRn ()
traceDFuns [ClsInst]
dfuns
      ; TcGblEnv
env <- IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
      ; (inst_env' :: InstEnv
inst_env', cls_insts' :: [ClsInst]
cls_insts') <- ((InstEnv, [ClsInst])
 -> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst]))
-> (InstEnv, [ClsInst])
-> [ClsInst]
-> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst
                                          (TcGblEnv -> InstEnv
tcg_inst_env TcGblEnv
env, TcGblEnv -> [ClsInst]
tcg_insts TcGblEnv
env)
                                          [ClsInst]
dfuns
      ; let env' :: TcGblEnv
env' = TcGblEnv
env { tcg_insts :: [ClsInst]
tcg_insts    = [ClsInst]
cls_insts'
                       , tcg_inst_env :: InstEnv
tcg_inst_env = InstEnv
inst_env' }
      ; TcGblEnv -> TcM a -> TcM a
forall gbl lcl a. gbl -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
setGblEnv TcGblEnv
env' TcM a
thing_inside }

addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
-- Check that the proposed new instance is OK,
-- and then add it to the home inst env
-- If overwrite_inst, then we can overwrite a direct match
addLocalInst :: (InstEnv, [ClsInst])
-> ClsInst -> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
addLocalInst (home_ie :: InstEnv
home_ie, my_insts :: [ClsInst]
my_insts) ispec :: ClsInst
ispec
   = do {
             -- Load imported instances, so that we report
             -- duplicates correctly

             -- 'matches'  are existing instance declarations that are less
             --            specific than the new one
             -- 'dups'     are those 'matches' that are equal to the new one
         ; Bool
isGHCi <- TcRn Bool
getIsGHCi
         ; ExternalPackageState
eps    <- TcRnIf TcGblEnv TcLclEnv ExternalPackageState
forall gbl lcl. TcRnIf gbl lcl ExternalPackageState
getEps
         ; TcGblEnv
tcg_env <- IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv

           -- In GHCi, we *override* any identical instances
           -- that are also defined in the interactive context
           -- See Note [Override identical instances in GHCi]
         ; let home_ie' :: InstEnv
home_ie'
                 | Bool
isGHCi    = InstEnv -> ClsInst -> InstEnv
deleteFromInstEnv InstEnv
home_ie ClsInst
ispec
                 | Bool
otherwise = InstEnv
home_ie

               global_ie :: InstEnv
global_ie = ExternalPackageState -> InstEnv
eps_inst_env ExternalPackageState
eps
               inst_envs :: InstEnvs
inst_envs = InstEnvs :: InstEnv -> InstEnv -> VisibleOrphanModules -> InstEnvs
InstEnvs { ie_global :: InstEnv
ie_global  = InstEnv
global_ie
                                    , ie_local :: InstEnv
ie_local   = InstEnv
home_ie'
                                    , ie_visible :: VisibleOrphanModules
ie_visible = TcGblEnv -> VisibleOrphanModules
tcVisibleOrphanMods TcGblEnv
tcg_env }

             -- Check for inconsistent functional dependencies
         ; let inconsistent_ispecs :: [ClsInst]
inconsistent_ispecs = InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs ClsInst
ispec
         ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
inconsistent_ispecs) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           ClsInst -> [ClsInst] -> TcRn ()
funDepErr ClsInst
ispec [ClsInst]
inconsistent_ispecs

             -- Check for duplicate instance decls.
         ; let (_tvs :: [Id]
_tvs, cls :: Class
cls, tys :: ThetaType
tys) = ClsInst -> ([Id], Class, ThetaType)
instanceHead ClsInst
ispec
               (matches :: [InstMatch]
matches, _, _)  = Bool
-> InstEnvs
-> Class
-> ThetaType
-> ([InstMatch], [ClsInst], [InstMatch])
lookupInstEnv Bool
False InstEnvs
inst_envs Class
cls ThetaType
tys
               dups :: [ClsInst]
dups             = (ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> Bool) -> [a] -> [a]
filter (ClsInst -> ClsInst -> Bool
identicalClsInstHead ClsInst
ispec) ((InstMatch -> ClsInst) -> [InstMatch] -> [ClsInst]
forall a b. (a -> b) -> [a] -> [b]
map InstMatch -> ClsInst
forall a b. (a, b) -> a
fst [InstMatch]
matches)
         ; Bool -> TcRn () -> TcRn ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ClsInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClsInst]
dups) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
           ClsInst -> ClsInst -> TcRn ()
dupInstErr ClsInst
ispec ([ClsInst] -> ClsInst
forall a. [a] -> a
head [ClsInst]
dups)

         ; (InstEnv, [ClsInst])
-> IOEnv (Env TcGblEnv TcLclEnv) (InstEnv, [ClsInst])
forall (m :: * -> *) a. Monad m => a -> m a
return (InstEnv -> ClsInst -> InstEnv
extendInstEnv InstEnv
home_ie' ClsInst
ispec, ClsInst
ispec ClsInst -> [ClsInst] -> [ClsInst]
forall a. a -> [a] -> [a]
: [ClsInst]
my_insts) }

{-
Note [Signature files and type class instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instances in signature files do not have an effect when compiling:
when you compile a signature against an implementation, you will
see the instances WHETHER OR NOT the instance is declared in
the file (this is because the signatures go in the EPS and we
can't filter them out easily.)  This is also why we cannot
place the instance in the hi file: it would show up as a duplicate,
and we don't have instance reexports anyway.

However, you might find them useful when typechecking against
a signature: the instance is a way of indicating to GHC that
some instance exists, in case downstream code uses it.

Implementing this is a little tricky.  Consider the following
situation (sigof03):

 module A where
     instance C T where ...

 module ASig where
     instance C T

When compiling ASig, A.hi is loaded, which brings its instances
into the EPS.  When we process the instance declaration in ASig,
we should ignore it for the purpose of doing a duplicate check,
since it's not actually a duplicate. But don't skip the check
entirely, we still want this to fail (tcfail221):

 module ASig where
     instance C T
     instance C T

Note that in some situations, the interface containing the type
class instances may not have been loaded yet at all.  The usual
situation when A imports another module which provides the
instances (sigof02m):

 module A(module B) where
     import B

See also Note [Signature lazy interface loading].  We can't
rely on this, however, since sometimes we'll have spurious
type class instances in the EPS, see #9422 (sigof02dm)

************************************************************************
*                                                                      *
        Errors and tracing
*                                                                      *
************************************************************************
-}

traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns :: [ClsInst] -> TcRn ()
traceDFuns ispecs :: [ClsInst]
ispecs
  = String -> SDoc -> TcRn ()
traceTc "Adding instances:" ([SDoc] -> SDoc
vcat ((ClsInst -> SDoc) -> [ClsInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ClsInst -> SDoc
pp [ClsInst]
ispecs))
  where
    pp :: ClsInst -> SDoc
pp ispec :: ClsInst
ispec = SDoc -> Int -> SDoc -> SDoc
hang (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ClsInst -> Id
instanceDFunId ClsInst
ispec) SDoc -> SDoc -> SDoc
<+> SDoc
colon)
                  2 (ClsInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInst
ispec)
        -- Print the dfun name itself too

funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
funDepErr ispec :: ClsInst
ispec ispecs :: [ClsInst]
ispecs
  = SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr (String -> SDoc
text "Functional dependencies conflict between instance declarations:")
                    (ClsInst
ispec ClsInst -> [ClsInst] -> [ClsInst]
forall a. a -> [a] -> [a]
: [ClsInst]
ispecs)

dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr :: ClsInst -> ClsInst -> TcRn ()
dupInstErr ispec :: ClsInst
ispec dup_ispec :: ClsInst
dup_ispec
  = SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr (String -> SDoc
text "Duplicate instance declarations:")
                    [ClsInst
ispec, ClsInst
dup_ispec]

addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
addClsInstsErr herald :: SDoc
herald ispecs :: [ClsInst]
ispecs
  = SrcSpan -> TcRn () -> TcRn ()
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan (ClsInst -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan ([ClsInst] -> ClsInst
forall a. [a] -> a
head [ClsInst]
sorted)) (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$
    SDoc -> TcRn ()
addErr (SDoc -> Int -> SDoc -> SDoc
hang SDoc
herald 2 ([ClsInst] -> SDoc
pprInstances [ClsInst]
sorted))
 where
   sorted :: [ClsInst]
sorted = (ClsInst -> SrcLoc) -> [ClsInst] -> [ClsInst]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith ClsInst -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc [ClsInst]
ispecs
   -- The sortWith just arranges that instances are dislayed in order
   -- of source location, which reduced wobbling in error messages,
   -- and is better for users