Commit abed9bf5 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix solving of implicit parameter constraints

Trac #14218 showed that we were not solving implicit-parameter
constraints correctly.  In particular,

- A tuple constraint could "hide" an implicit-parameter wanted
  constraint, and that in turn could that we solved it from the
  wrong implicit-parameter binding.

- As a special case the HasCallStack constraint (which is just
  short for (IP "callStack" CallStack), was getting mis-solved.

The big change is to arrange that, in TcSMonad.findDict when looking
for a dictionary, either when looking for a matching inert or solved
dictionary, we fail for

  - Tuples that are hiding implicit parameters
    See Note [Tuples hiding implicit parameters]

  - HasCallStack constraints where we have not yet pushed
    on the call-site info
    See Note [Solving CallStack constraints]

I also did a little refactoring

* Move naturallyCoherentClass from Class to TcInteract, its sole
  use site.  Class.hs seems like the wrong place.  (And I also
  do not understand the reason that we need the eq/Coercible/
  Typable stuff in this predicate, but I'll tackle that separately.)

* Move the code that pushes call-site info onto a call stack
  from the "interact" part to the "canonicalise" part of the solver.
parent 1b476ab5
......@@ -4,7 +4,8 @@ module TcCanonical(
canonicalize,
unifyDerived,
makeSuperClasses, maybeSym,
StopOrContinue(..), stopWith, continueWith
StopOrContinue(..), stopWith, continueWith,
solveCallStack -- For TcSimplify
) where
#include "HsVersions.h"
......@@ -30,6 +31,7 @@ import Outputable
import DynFlags( DynFlags )
import NameSet
import RdrName
import HsTypes( HsIPName(..) )
import Pair
import Util
......@@ -134,10 +136,47 @@ canClassNC ev cls tys
= do { sc_cts <- mkStrictSuperClasses ev cls tys
; emitWork sc_cts
; canClass ev cls tys False }
| isWanted ev
, Just ip_name <- isCallStackPred cls tys
, OccurrenceOf func <- ctLocOrigin loc
-- If we're given a CallStack constraint that arose from a function
-- call, we need to push the current call-site onto the stack instead
-- of solving it directly from a given.
-- See Note [Overview of implicit CallStacks] in TcEvidence
-- and Note [Solving CallStack constraints] in TcSMonad
= do { -- First we emit a new constraint that will capture the
-- given CallStack.
; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
-- We change the origin to IPOccOrigin so
-- this rule does not fire again.
-- See Note [Overview of implicit CallStacks]
; new_ev <- newWantedEvVarNC new_loc pred
-- Then we solve the wanted by pushing the call-site
-- onto the newly emitted CallStack
; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvTerm new_ev)
; solveCallStack ev ev_cs
; canClass new_ev cls tys False }
| otherwise
= canClass ev cls tys (has_scs cls)
where
has_scs cls = not (null (classSCTheta cls))
loc = ctEvLoc ev
pred = ctEvPred ev
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
-- Also called from TcSimplify when defaulting call stacks
solveCallStack ev ev_cs = do
-- We're given ev_cs :: CallStack, but the evidence term should be a
-- dictionary, so we have to coerce ev_cs to a dictionary for
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvId ev) ev_tm
canClass :: CtEvidence
-> Class -> [Type]
......
......@@ -3,8 +3,6 @@
module TcInteract (
solveSimpleGivens, -- Solves [Ct]
solveSimpleWanteds, -- Solves Cts
solveCallStack, -- for use in TcSimplify
) where
#include "HsVersions.h"
......@@ -13,7 +11,6 @@ import GhcPrelude
import BasicTypes ( SwapFlag(..), isSwapped,
infinity, IntWithInf, intGtLimit )
import HsTypes ( HsIPName(..) )
import TcCanonical
import TcFlatten
import TcUnify( canSolveByUnification )
......@@ -30,9 +27,10 @@ import TcType
import Name
import RdrName ( lookupGRE_FieldLabel )
import PrelNames ( knownNatClassName, knownSymbolClassName,
typeableClassName, coercibleTyConKey,
typeableClassName, typeableClassKey,
coercibleTyConKey,
hasFieldClassName,
heqTyConKey, ipClassKey )
heqTyConKey, eqTyConKey, ipClassKey )
import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
coercibleDataCon, constraintKindTyCon )
import TysPrim ( eqPrimTyCon, eqReprPrimTyCon )
......@@ -837,59 +835,38 @@ It is important to emphasize that failure means that we don't produce more
efficient code, NOT that we fail to typecheck at all! This is purely an
an optimization: exactly the same programs should typecheck with or without this
procedure.
-}
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
| isWanted ev_w
, Just ip_name <- isCallStackPred (ctPred workItem)
, OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
-- If we're given a CallStack constraint that arose from a function
-- call, we need to push the current call-site onto the stack instead
-- of solving it directly from a given.
-- See Note [Overview of implicit CallStacks]
= do { let loc = ctEvLoc ev_w
-- First we emit a new constraint that will capture the
-- given CallStack.
; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
-- We change the origin to IPOccOrigin so
-- this rule does not fire again.
-- See Note [Overview of implicit CallStacks]
; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
; emitWorkNC (freshGoals [mb_new])
-- Then we solve the wanted by pushing the call-site onto the
-- newly emitted CallStack.
; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
; solveCallStack ev_w ev_cs
; stopWith ev_w "Wanted CallStack IP" }
| Just ctev_i <- lookupInertDict inerts cls tys
= do
{ dflags <- getDynFlags
-- See Note [Solving from instances when interacting Dicts]
; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
; case try_inst_res of
Just evs -> do
{ flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
{ setWantedEvBind (ctEvId ct_ev) ev_t
; addSolvedDict ct_ev cls typ }
; stopWith ev_w "interactDict/solved from instance" }
-- We were unable to solve the [W] constraint from in-scope instances so
-- we solve it from the solution in the inerts we just retrieved.
Nothing -> do
{ (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
; case inert_effect of
IRKeep -> return ()
IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
; if stop_now then
return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
else
continueWith workItem } }
| Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
= -- There is a matching dictionary in the inert set
do { -- First to try to solve it /completely/ from
-- top level instances
-- See Note [Solving from instances when interacting Dicts]
dflags <- getDynFlags
; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
; case try_inst_res of
Just evs -> do
{ flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
{ setWantedEvBind (ctEvId ct_ev) ev_t
; addSolvedDict ct_ev cls typ }
; stopWith ev_w "interactDict/solved from instance" }
-- We were unable to solve the [W] constraint from in-scope instances
-- so we solve it from the matching inert we found
Nothing -> do
{ (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
; case inert_effect of
IRKeep -> return ()
IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
; if stop_now then
return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
else
continueWith workItem } }
| cls `hasKey` ipClassKey
, isGiven ev_w
= interactGivenIP inerts workItem
......@@ -936,7 +913,7 @@ trySolveFromInstance dflags ev_w ctev_i
new_wanted_cached :: DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached cache pty
| ClassPred cls tys <- classifyPredType pty
= lift $ case findDict cache cls tys of
= lift $ case findDict cache loc_w cls tys of
Just ctev -> return $ Cached (ctEvTerm ctev)
Nothing -> Fresh <$> newWantedNC loc_w pty
| otherwise = mzero
......@@ -1037,7 +1014,6 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
{- Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
......@@ -2075,7 +2051,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
= do { try_fundep_improvement
; continueWith work_item }
| Just ev <- lookupSolvedDict inerts cls xis -- Cached
| Just ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
= do { setEvBindIfWanted fl (ctEvTerm ev)
; stopWith fl "Dict/Top (cached)" }
......@@ -2207,6 +2183,17 @@ match_class_inst dflags clas tys loc
where
cls_name = className clas
-- | If a class is "naturally coherent", then we needn't worry at all, in any
-- way, about overlapping/incoherent instances. Just solve the thing!
naturallyCoherentClass :: Class -> Bool
-- See also Note [The equality class story] in TysPrim.
naturallyCoherentClass cls
= isCTupleClass cls || -- See "Tuple classes" in Note [Instance and Given overlap]
cls `hasKey` heqTyConKey ||
cls `hasKey` eqTyConKey ||
cls `hasKey` coercibleTyConKey ||
cls `hasKey` typeableClassKey
{- Note [Instance and Given overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Example, from the OutsideIn(X) paper:
......@@ -2262,6 +2249,15 @@ Other notes:
* Another "live" example is Trac #10195; another is #10177.
* Tuple classes. For reasons described in TcSMonad
Note [Tuples hiding implicit parameters], we may have a constraint
[W] (?x::Int, C a)
with an exactly-matching Given constraint. We must decompose this
tuple and solve the components separately, otherwise we won't solve
it at all! It is perfectly safe to decompose it, because the "instance"
for class tuples is bidirectional: the Given can also be decomposed
to provide the pieces.
* We ignore the overlap problem if -XIncoherentInstances is in force:
see Trac #6002 for a worked-out example where this makes a
difference.
......@@ -2531,14 +2527,6 @@ a TypeRep for them. For qualified but not polymorphic types, like
For now we leave it off, until we have a better story for impredicativity.
-}
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack ev ev_cs = do
-- We're given ev_cs :: CallStack, but the evidence term should be a
-- dictionary, so we have to coerce ev_cs to a dictionary for
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvId ev) ev_tm
{- ********************************************************************
* *
Class lookup for lifted equality
......
......@@ -2015,30 +2015,30 @@ lookupFlatCache fam_tc tys
lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
lookupInInerts pty
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
; return (lookupSolvedDict inerts cls tys `mplus`
lookupInertDict (inert_cans inerts) cls tys) }
; return (lookupSolvedDict inerts loc cls tys `mplus`
lookupInertDict (inert_cans inerts) loc cls tys) }
| otherwise -- NB: No caching for equalities, IPs, holes, or errors
= return Nothing
-- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not
-- match the input exactly. Note [Use loose types in inert set].
lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) cls tys
= case findDict dicts cls tys of
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
= case findDict dicts loc cls tys of
Just ct -> Just (ctEvidence ct)
_ -> Nothing
-- | Look up a solved inert. NB: the returned 'CtEvidence' might not
-- match the input exactly. See Note [Use loose types in inert set].
lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
= case findDict solved cls tys of
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
= case findDict solved loc cls tys of
Just ev -> Just ev
_ -> Nothing
......@@ -2125,16 +2125,66 @@ foldTcAppMap k m z = foldUDFM (foldTM k) z m
* *
********************************************************************* -}
{- Note [Tuples hiding implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f,g :: (?x::Int, C a) => a -> a
f v = let ?x = 4 in g v
The call to 'g' gives rise to a Wanted contraint (?x::Int, C a).
We must /not/ solve this from the Given (?x::Int, C a), because of
the intervening binding for (?x::Int). Trac #14218.
We deal with this by arranging that we always fail when looking up a
tuple constraint that hides an implicit parameter. Not that this applies
* both to the inert_dicts (lookupInertDict)
* and to the solved_dicts (looukpSolvedDict)
An alternative would be not to extend these sets with such tuple
constraints, but it seemed more direct to deal with the lookup.
Note [Solving CallStack constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose f :: HasCallStack => blah. Then
* Each call to 'f' gives rise to
[W] s1 :: IP "callStack" CallStack -- CtOrigin = OccurrenceOf f
with a CtOrigin that says "OccurrenceOf f".
Remember that HasCallStack is just shorthand for
IP "callStack CallStack
See Note [Overview of implicit CallStacks] in TcEvidence
* We cannonicalise such constraints, in TcCanonical.canClassNC, by
pushing the call-site info on the stack, and changing the CtOrigin
to record that has been done.
Bind: s1 = pushCallStack <site-info> s2
[W] s2 :: IP "callStack" CallStack -- CtOrigin = IPOccOrigin
* Then, and only then, we can solve the contraint from an enclosing
Given.
So we must be careful /not/ to solve 's1' from the Givens. Again,
we ensure this by arranging that findDict always misses when looking
up souch constraints.
-}
type DictMap a = TcAppMap a
emptyDictMap :: DictMap a
emptyDictMap = emptyTcAppMap
-- sizeDictMap :: DictMap a -> Int
-- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict m loc cls tys
| isCTupleClass cls
, any hasIPPred tys -- See Note [Tuples hiding implicit parameters]
= Nothing
findDict :: DictMap a -> Class -> [Type] -> Maybe a
findDict m cls tys = findTcApp m (getUnique cls) tys
| Just {} <- isCallStackPred cls tys
, OccurrenceOf {} <- ctLocOrigin loc
= Nothing -- See Note [Solving CallStack constraints]
| otherwise
= findTcApp m (getUnique cls) tys
findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass m cls
......@@ -3084,7 +3134,7 @@ newWantedEvVarNC loc pty
newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
-- For anything except ClassPred, this is the same as newWantedEvVarNC
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts pty
= do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev
| not (isDerived ctev)
......
......@@ -36,7 +36,7 @@ import PrelNames
import TcErrors
import TcEvidence
import TcInteract
import TcCanonical ( makeSuperClasses )
import TcCanonical ( makeSuperClasses, solveCallStack )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
......@@ -224,7 +224,8 @@ defaultCallStacks wanteds
; setImplicationStatus (implic { ic_wanted = wanteds }) }
defaultCallStack ct
| Just _ <- isCallStackPred (ctPred ct)
| ClassPred cls tys <- classifyPredType (ctPred ct)
, Just {} <- isCallStackPred cls tys
= do { solveCallStack (cc_ev ct) EvCsEmpty
; return Nothing }
......
......@@ -78,7 +78,7 @@ module TcType (
isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarExposed, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead,
isRigidEqPred, isRigidTy,
......@@ -1877,7 +1877,7 @@ pickQuantifiablePreds qtvs theta
= case classifyPredType pred of
ClassPred cls tys
| Just {} <- isCallStackPred pred
| Just {} <- isCallStackPred cls tys
-- NEVER infer a CallStack constraint
-- Otherwise, we let the constraints bubble up to be
-- solved from the outer context, or be defaulted when we
......@@ -2120,14 +2120,23 @@ isCallStackTy ty
-- | Is a 'PredType' a 'CallStack' implicit parameter?
--
-- If so, return the name of the parameter.
isCallStackPred :: PredType -> Maybe FastString
isCallStackPred pred
| Just (str, ty) <- isIPPred_maybe pred
, isCallStackTy ty
= Just str
isCallStackPred :: Class -> [Type] -> Maybe FastString
isCallStackPred cls tys
| [ty1, ty2] <- tys
, isIPClass cls
, isCallStackTy ty2
= isStrLitTy ty1
| otherwise
= Nothing
hasIPPred :: PredType -> Bool
hasIPPred pred
= case classifyPredType pred of
ClassPred cls tys
| isIPClass cls -> True
| isCTupleClass cls -> any hasIPPred tys
_other -> False
is_tc :: Unique -> Type -> Bool
-- Newtypes are opaque to this
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
......
......@@ -19,7 +19,6 @@ module Class (
classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
classAllSelIds, classSCSelId, classMinimalDef, classHasFds,
isAbstractClass,
naturallyCoherentClass
) where
#include "HsVersions.h"
......@@ -34,8 +33,6 @@ import BasicTypes
import Unique
import Util
import SrcLoc
import PrelNames ( eqTyConKey, coercibleTyConKey, typeableClassKey,
heqTyConKey )
import Outputable
import BooleanFormula (BooleanFormula, mkTrue)
......@@ -313,16 +310,6 @@ isAbstractClass :: Class -> Bool
isAbstractClass Class{ classBody = AbstractClass } = True
isAbstractClass _ = False
-- | If a class is "naturally coherent", then we needn't worry at all, in any
-- way, about overlapping/incoherent instances. Just solve the thing!
naturallyCoherentClass :: Class -> Bool
-- See also Note [The equality class story] in TysPrim.
naturallyCoherentClass cls
= cls `hasKey` heqTyConKey ||
cls `hasKey` eqTyConKey ||
cls `hasKey` coercibleTyConKey ||
cls `hasKey` typeableClassKey
{-
************************************************************************
* *
......
{-# LANGUAGE ConstraintKinds #-} -- For 'C'
{-# LANGUAGE MultiParamTypeClasses #-} -- For nullary 'Trivial' class
{-# LANGUAGE ImplicitParams #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
module Main where
import qualified GHC.Stack as Ghc
class Trivial where
instance Trivial where
type C = (Ghc.HasCallStack, Trivial)
-- | Print the functions on the call stack.
callStack :: C => IO ()
callStack = print $ map fst (Ghc.getCallStack Ghc.callStack)
f :: C => a -> IO ()
f x = callStack
type C2 = (?x::Int, ?y::Int)
h1 :: C2 => Int -> IO ()
h1 v = print (?x+v)
h2 :: C2 => Int -> IO ()
h2 v = let ?x = 0 in h1 v
main = do { let { ?x = 3; ?y = 4 } in h2 4
-- Should print 4+0 = 4
; f "ugh"
-- Should print @["callStack", "f"]@.
}
......@@ -123,3 +123,4 @@ test('TypeableEq', normal, compile_and_run, [''])
test('T13435', normal, compile_and_run, [''])
test('T11715', exit_code(1), compile_and_run, [''])
test('T13594a', normal, ghci_script, ['T13594a.script'])
test('T14218', normal, compile_and_run, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment