Commit a2a9006b authored by xldenis's avatar xldenis Committed by Marge Bot

Fix issue #18262 by zonking constraints after solving

Zonk residual constraints in checkForExistence to reveal user type

Previously when `:instances` was used with instances that have TypeError
constraints the result would look something like:

instance [safe] s0 => Err 'A -- Defined at ../Bug2.hs:8:10

whereas after zonking, `:instances` now sees the `TypeError` and
properly eliminates the constraint from the results.
parent cad62ef1
Pipeline #21357 failed with stages
in 431 minutes and 16 seconds
......@@ -118,11 +118,8 @@ import GHC.Tc.Module ( runTcInteractive, tcRnType, loadUnqualIfaces )
import GHC.Tc.Utils.Zonk ( ZonkFlexi (SkolemiseFlexi) )
import GHC.Tc.Utils.Env (tcGetInstEnvs)
import GHC.Tc.Utils.Instantiate (instDFunType)
import GHC.Tc.Solver (solveWanteds)
import GHC.Tc.Solver (simplifyWantedsTcM)
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Evidence
import Data.Bifunctor (second)
import GHC.Tc.Solver.Monad (runTcS)
import GHC.Core.Class (classTyCon)
-- -----------------------------------------------------------------------------
......@@ -1069,24 +1066,22 @@ parseInstanceHead str = withSession $ \hsc_env0 -> do
return ty
-- Get all the constraints required of a dictionary binding
getDictionaryBindings :: PredType -> TcM WantedConstraints
getDictionaryBindings :: PredType -> TcM CtEvidence
getDictionaryBindings theta = do
dictName <- newName (mkDictOcc (mkVarOcc "magic"))
let dict_var = mkVanillaGlobal dictName theta
loc <- getCtLocM (GivenOrigin UnkSkol) Nothing
-- Generate a wanted constraint here because at the end of constraint
-- Generate a wanted here because at the end of constraint
-- solving, most derived constraints get thrown away, which in certain
-- cases, notably with quantified constraints makes it impossible to rule
-- out instances as invalid. (See #18071)
let wCs = mkSimpleWC [CtWanted {
return CtWanted {
ctev_pred = varType dict_var,
ctev_dest = EvVarDest dict_var,
ctev_nosh = WDeriv,
ctev_loc = loc
return wCs
-- Find instances where the head unifies with the provided type
findMatchingInstances :: Type -> TcM [(ClsInst, [DFunInstType])]
......@@ -1142,17 +1137,18 @@ checkForExistence clsInst mb_inst_tys = do
-- thetas of clsInst.
(tys, thetas) <- instDFunType (is_dfun clsInst) mb_inst_tys
wanteds <- mapM getDictionaryBindings thetas
(residuals, _) <- second evBindMapBinds <$> runTcS (solveWanteds (unionsWC wanteds))
let WC { wc_simple = simples, wc_impl = impls } = (dropDerivedWC residuals)
-- It's important to zonk constraints after solving in order to expose things like TypeErrors
-- which otherwise appear as opaque type variables. (See #18262).
WC { wc_simple = simples, wc_impl = impls } <- simplifyWantedsTcM wanteds
let resPreds = mapBag ctPred simples
if allBag isSatisfiablePred resPreds && solvedImplics impls
then return . Just $ substInstArgs tys (bagToList resPreds) clsInst
if allBag allowedSimple simples && solvedImplics impls
then return . Just $ substInstArgs tys (bagToList (mapBag ctPred simples)) clsInst
else return Nothing
allowedSimple :: Ct -> Bool
allowedSimple ct = isSatisfiablePred (ctPred ct)
solvedImplics :: Bag Implication -> Bool
solvedImplics impls = allBag (isSolvedStatus . ic_status) impls
......@@ -2518,6 +2518,25 @@ commonly used commands.
instance Show _ => Show (Maybe _) -- Defined in ‘GHC.Show’
instance Read _ => Read (Maybe _) -- Defined in ‘GHC.Read’
Only instances which could potentially be used will be displayed in the results.
Instances which require unsatisfiable constraints such as ``TypeError`` will not be
included. In the following example, the instance for ``A`` is not shown because it cannot
be used.
.. code-block:: none
ghci>:set -XDataKinds -XUndecidableInstances
ghci>import GHC.TypeLits
ghci>class A a
ghci>instance (TypeError (Text "Not possible")) => A Bool
ghci>:instances Bool
instance Eq Bool -- Defined in ‘GHC.Classes’
instance Ord Bool -- Defined in ‘GHC.Classes’
instance Enum Bool -- Defined in ‘GHC.Enum’
instance Show Bool -- Defined in ‘GHC.Show’
instance Read Bool -- Defined in ‘GHC.Read’
instance Bounded Bool -- Defined in ‘GHC.Enum’
.. ghci-cmd:: :issafe; [⟨module⟩]
Displays Safe Haskell information about the given module (or the
{-# LANGUAGE TypeFamilies, FlexibleInstances, DataKinds, UndecidableInstances #-}
import GHC.TypeLits
data C = A | B
class Err (a :: C)
instance (TypeError ('Text "uh-oh")) => Err 'A
instance Err 'B
:load T18262.hs
:set -XDataKinds
-- Should report no instances
:instances 'A
-- Should report an instance with no constraints
:instances 'B
instance [safe] Err 'B -- Defined at T18262.hs:10:10
test('T18262', [extra_files(['T18262.hs'])], ghci_script, ['T18262.script'])
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment