Instances in no-evidence implications
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 22 Jun 2018 10:27:47 +0000 (11:27 +0100)
committerBen Gamari <ben@smart-cactus.org>
Wed, 27 Jun 2018 21:07:55 +0000 (17:07 -0400)
Trac #15290 showed that it's possible that we might attempt to use a
quantified constraint to solve an equality in a situation where we
don't have anywhere to put the evidence bindings.  This made GHC crash.

This patch stops the crash, but still rejects the pogram.  See
Note [Instances in no-evidence implications] in TcInteract.

Finding this bug revealed another lurking bug:

* An infelicity in the treatment of superclasses -- we were expanding
  them locally at the leaves, rather than at their binding site; see
  (3a) in Note [The superclass story].

  As a consequence, TcRnTypes.superclassesMightHelp must look inside
  implications.

In more detail:

* Stop the crash, by making TcInteract.chooseInstance test for
  the no-evidence-bindings case.  In that case we simply don't
  use the instance.  This entailed a slight change to the type
  of chooseInstance.

* Make TcSMonad.getPendingScDicts (now renamed getPendingGivenScs)
  return only Givens from the /current level/; and make
  TcRnTypes.superClassesMightHelp look inside implications.

* Refactor the simpl_loop and superclass-expansion stuff in
  TcSimplify.  The logic is much easier to understand now, and
  has less duplication.

(cherry picked from commit 32eb41994f7448caf5fb6b06ed0678d79d029deb)

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/quantified-constraints/T15290.hs [new file with mode: 0644]
testsuite/tests/quantified-constraints/T15290a.hs [new file with mode: 0644]
testsuite/tests/quantified-constraints/T15290a.stderr [new file with mode: 0644]
testsuite/tests/quantified-constraints/all.T

index b0ff962..a8fff6b 100644 (file)
@@ -289,6 +289,15 @@ So here's the plan:
    This may succeed in generating (a finite number of) extra Givens,
    and extra Deriveds. Both may help the proof.
 
+3a An important wrinkle: only expand Givens from the current level.
+   Two reasons:
+      - We only want to expand it once, and that is best done at
+        the level it is bound, rather than repeatedly at the leaves
+        of the implication tree
+      - We may be inside a type where we can't create term-level
+        evidence anyway, so we can't superclass-expand, say,
+        (a ~ b) to get (a ~# b).  This happened in Trac #15290.
+
 4. Go round to (2) again.  This loop (2,3,4) is implemented
    in TcSimplify.simpl_loop.
 
index f20a17b..2ad93b0 100644 (file)
@@ -1840,7 +1840,7 @@ doTopReactOther work_item
   = do { -- Try local quantified constraints
          res <- matchLocalInst pred (ctEvLoc ev)
        ; case res of
-           OneInst {} -> chooseInstance ev pred res
+           OneInst {} -> chooseInstance work_item res
            _          -> continueWith work_item }
   where
     ev = ctEvidence work_item
@@ -2235,7 +2235,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                OneInst { lir_safe_over = s }
                   -> do { unless s $ insertSafeOverlapFailureTcS work_item
                         ; when (isWanted ev) $ addSolvedDict ev cls xis
-                        ; chooseInstance ev dict_pred lkup_res }
+                        ; chooseInstance work_item lkup_res }
                _  ->  -- NoInstance or NotSure
                      do { when (isImprovable ev) $
                           try_fundep_improvement
@@ -2264,9 +2264,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
 
-chooseInstance :: CtEvidence -> TcPredType -> LookupInstResult
-               -> TcS (StopOrContinue Ct)
-chooseInstance ev pred
+chooseInstance :: Ct -> LookupInstResult -> TcS (StopOrContinue Ct)
+chooseInstance work_item
                (OneInst { lir_new_theta = theta
                         , lir_mk_ev     = mk_ev })
   = do { traceTcS "doTopReact/found instance for" $ ppr ev
@@ -2274,9 +2273,11 @@ chooseInstance ev pred
        ; if isDerived ev then finish_derived theta
                          else finish_wanted  theta mk_ev }
   where
+     ev         = ctEvidence work_item
+     pred       = ctEvPred ev
      loc        = ctEvLoc ev
-     deeper_loc = zap_origin (bumpCtLocDepth loc)
      origin     = ctLocOrigin loc
+     deeper_loc = zap_origin (bumpCtLocDepth loc)
 
      zap_origin loc  -- After applying an instance we can set ScOrigin to
                      -- infinity, so that prohibitedSuperClassSolve never fires
@@ -2289,10 +2290,15 @@ chooseInstance ev pred
                    -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
      finish_wanted theta mk_ev
-        = do { evc_vars <- mapM (newWanted deeper_loc) theta
+        = do { evb <- getTcEvBindsVar
+             ; if isNoEvBindsVar evb
+               then -- See Note [Instances in no-evidence implications]
+                    continueWith work_item
+               else
+          do { evc_vars <- mapM (newWanted deeper_loc) theta
              ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith ev "Dict/Top (solved wanted)" }
+             ; stopWith ev "Dict/Top (solved wanted)" } }
 
      finish_derived theta  -- Use type-class instances for Deriveds, in the hope
        =                   -- of generating some improvements
@@ -2302,8 +2308,28 @@ chooseInstance ev pred
             ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
             ; stopWith ev "Dict/Top (solved derived)" }
 
-chooseInstance ev _ lookup_res
-  = pprPanic "chooseInstance" (ppr ev $$ ppr lookup_res)
+chooseInstance work_item lookup_res
+  = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
+
+{- Note [Instances in no-evidence implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In Trac #15290 we had
+  [G] forall p q. Coercible p q => Coercible (m p) (m q))
+  [W] forall <no-ev> a. m (Int, IntStateT m a)
+                          ~R#
+                        m (Int, StateT Int m a)
+
+The Given is an ordinary quantified constraint; the Wanted is an implication
+equality that arises from
+  [W] (forall a. t1) ~R# (forall a. t2)
+
+But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
+we can't generate any term evidence.  So we can't actually use that
+lovely quantified constraint.  Alas!
+
+This test arranges to ignore the instance-based solution under these
+(rare) circumstances.   It's sad, but I  really don't see what else we can do.
+-}
 
 {- *******************************************************************
 *                                                                    *
index d54d71f..0a443a0 100644 (file)
@@ -71,7 +71,7 @@ module TcRnTypes(
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts, isCTyEqCan, isCFunEqCan,
-        isPendingScDict, superClassesMightHelp,
+        isPendingScDict, superClassesMightHelp, getPendingWantedScs,
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCNonCanonical, isWantedCt, isDerivedCt,
         isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
@@ -2214,16 +2214,31 @@ setPendingScDict ct@(CDictCan { cc_pend_sc = False })
                     = ct { cc_pend_sc = True }
 setPendingScDict ct = ct
 
-superClassesMightHelp :: Ct -> Bool
+superClassesMightHelp :: WantedConstraints -> Bool
 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
 -- expose more equalities or functional dependencies) might help to
 -- solve this constraint.  See Note [When superclasses help]
-superClassesMightHelp ct
-  = isWantedCt ct && not (is_ip ct)
+superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
+  = anyBag might_help_ct simples || anyBag might_help_implic implics
   where
+    might_help_implic ic
+       | IC_Unsolved <- ic_status ic = superClassesMightHelp (ic_wanted ic)
+       | otherwise                   = False
+
+    might_help_ct ct = isWantedCt ct && not (is_ip ct)
+
     is_ip (CDictCan { cc_class = cls }) = isIPClass cls
     is_ip _                             = False
 
+getPendingWantedScs :: Cts -> ([Ct], Cts)
+getPendingWantedScs simples
+  = mapAccumBagL get [] simples
+  where
+    get acc ct | Just ct' <- isPendingScDict ct
+               = (ct':acc, ct')
+               | otherwise
+               = (acc,     ct)
+
 {- Note [When superclasses help]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 First read Note [The superclass story] in TcCanonical.
@@ -2234,6 +2249,11 @@ might actually help. The function superClassesMightHelp tells if
 doing this superclass expansion might help solve this constraint.
 Note that
 
+  * We look inside implications; maybe it'll help to expand the Givens
+    at level 2 to help solve an unsolved Wanted buried inside an
+    implication.  E.g.
+        forall a. Ord a => forall b. [W] Eq a
+
   * Superclasses help only for Wanted constraints.  Derived constraints
     are not really "unsolved" and we certainly don't want them to
     trigger superclass expansion. This was a good part of the loop
index b1865e8..965bf5f 100644 (file)
@@ -58,7 +58,7 @@ module TcSMonad (
     getTcSInerts, setTcSInerts,
     matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
     getUnsolvedInerts,
-    removeInertCts, getPendingScDicts,
+    removeInertCts, getPendingGivenScs,
     addInertCan, insertFunEq, addInertForAll,
     emitWorkNC, emitWork,
     isImprovable,
@@ -1935,27 +1935,36 @@ getInertGivens
                      $ concat (dVarEnvElts (inert_eqs inerts))
        ; return (filter isGivenCt all_cts) }
 
-getPendingScDicts :: TcS [Ct]
--- Find all inert Given dictionaries whose cc_pend_sc flag is True
--- Set the flag to False in the inert set, and return that Ct
-getPendingScDicts = updRetInertCans get_sc_dicts
+getPendingGivenScs :: TcS [Ct]
+-- Find all inert Given dictionaries, or quantified constraints,
+--     whose cc_pend_sc flag is True
+--     and that belong to the current level
+-- Set their cc_pend_sc flag to False in the inert set, and return that Ct
+getPendingGivenScs = do { lvl <- getTcLevel
+                        ; updRetInertCans (get_sc_pending lvl) }
+
+get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
+get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
+  = ASSERT2( all isGivenCt sc_pending, ppr sc_pending )
+       -- When getPendingScDics is called,
+       -- there are never any Wanteds in the inert set
+    (sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
   where
-    get_sc_dicts ic@(IC { inert_dicts = dicts, inert_insts = insts })
-      = (sc_pend_insts ++ sc_pend_dicts, ic')
-      where
-        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts
-                 , inert_insts = insts' }
+    sc_pending = sc_pend_insts ++ sc_pend_dicts
 
-        sc_pend_dicts :: [Ct]
-        sc_pend_dicts = foldDicts get_pending dicts []
+    sc_pend_dicts = foldDicts get_pending dicts []
+    dicts' = foldr add dicts sc_pend_dicts
 
-        (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
+    (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
 
     get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
                                        -- but flipping the flag
     get_pending dict dicts
-        | Just dict' <- isPendingScDict dict = dict' : dicts
-        | otherwise                          = dicts
+        | Just dict' <- isPendingScDict dict
+        , belongs_to_this_level (ctEvidence dict)
+        = dict' : dicts
+        | otherwise
+        = dicts
 
     add :: Ct -> DictMap Ct -> DictMap Ct
     add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
@@ -1963,12 +1972,17 @@ getPendingScDicts = updRetInertCans get_sc_dicts
     add ct _ = pprPanic "getPendingScDicts" (ppr ct)
 
     get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
-    get_pending_inst cts qci
+    get_pending_inst cts qci@(QCI { qci_ev = ev })
        | Just qci' <- isPendingScInst qci
+       , belongs_to_this_level ev
        = (CQuantCan qci' : cts, qci')
        | otherwise
        = (cts, qci)
 
+    belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl
+    -- We only want Givens from this level; see (3a) in
+    -- Note [The superclass story] in TcCanonical
+
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
                          , Cts     -- Fun eqs:   F a ~ ty
index 0514acd..c6e5a6e 100644 (file)
@@ -537,7 +537,7 @@ tcCheckSatisfiability given_ids
       | not (isEmptyBag insols)   -- We've found that it's definitely unsatisfiable
       = return insols             -- Hurrah -- stop now.
       | otherwise
-      = do { pending_given <- getPendingScDicts
+      = do { pending_given <- getPendingGivenScs
            ; new_given <- makeSuperClasses pending_given
            ; solveSimpleGivens new_given
            ; getInertInsols }
@@ -1374,19 +1374,12 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
                 -- Any insoluble constraints are in 'simples' and so get rewritten
                 -- See Note [Rewrite insolubles] in TcSMonad
 
-       ; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
+       ; (floated_eqs, implics2) <- solveNestedImplications $
+                                    implics `unionBags` wc_impl wc1
 
-       ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
-       ; (no_new_scs, simples2)  <- expandSuperClasses simples1
-
-       ; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
-                                               , text "simples2 =" <+> ppr simples2 ]
-
-       ; dflags <- getDynFlags
+       ; dflags   <- getDynFlags
        ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
-                                no_new_scs
-                                (WC { wc_simple = simples2
-                                    , wc_impl   = implics2 })
+                                (wc1 { wc_impl = implics2 })
 
        ; ev_binds_var <- getTcEvBindsVar
        ; bb <- TcS.getTcEvBindsMap ev_binds_var
@@ -1396,14 +1389,9 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
 
        ; return final_wc }
 
-simpl_loop :: Int -> IntWithInf -> Cts -> Bool
-           -> WantedConstraints
-           -> TcS WantedConstraints
-simpl_loop n limit floated_eqs no_new_deriveds
-           wc@(WC { wc_simple = simples, wc_impl = implics })
-  | isEmptyBag floated_eqs && no_new_deriveds
-  = return wc  -- Done!
-
+simpl_loop :: Int -> IntWithInf -> Cts
+           -> WantedConstraints -> TcS WantedConstraints
+simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
   | n `intGtLimit` limit
   = do { -- Add an error (not a warning) if we blow the limit,
          -- Typically if we blow the limit we are going to report some other error
@@ -1414,75 +1402,67 @@ simpl_loop n limit floated_eqs no_new_deriveds
                 2 (vcat [ text "Unsolved:" <+> ppr wc
                         , ppUnless (isEmptyBag floated_eqs) $
                           text "Floated equalities:" <+> ppr floated_eqs
-                        , ppUnless no_new_deriveds $
-                          text "New deriveds found"
                         , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
                   ]))
        ; return wc }
 
+  | not (isEmptyBag floated_eqs)
+  = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
+            -- Put floated_eqs first so they get solved first
+            -- NB: the floated_eqs may include /derived/ equalities
+            -- arising from fundeps inside an implication
+
+  | superClassesMightHelp wc
+  = -- We still have unsolved goals, and apparently no way to solve them,
+    -- so try expanding superclasses at this level, both Given and Wanted
+    do { pending_given <- getPendingGivenScs
+       ; let (pending_wanted, simples1) = getPendingWantedScs simples
+       ; if null pending_given && null pending_wanted
+           then return wc  -- After all, superclasses did not help
+           else
+    do { new_given  <- makeSuperClasses pending_given
+       ; new_wanted <- makeSuperClasses pending_wanted
+       ; solveSimpleGivens new_given -- Add the new Givens to the inert set
+       ; simplify_again n limit (null pending_given)
+         wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
+
   | otherwise
-  = do { let n_floated = lengthBag floated_eqs
-       ; csTraceTcS $
+  = return wc
+
+simplify_again :: Int -> IntWithInf -> Bool
+               -> WantedConstraints -> TcS WantedConstraints
+-- We have definitely decided to have another go at solving
+-- the wanted constraints (we have tried at least once already
+simplify_again n limit no_new_given_scs
+               wc@(WC { wc_simple = simples, wc_impl = implics })
+  = do { csTraceTcS $
          text "simpl_loop iteration=" <> int n
-         <+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
-                            , int n_floated <+> text "floated eqs" <> comma
+         <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
                             , int (lengthBag simples) <+> text "simples to solve" ])
+       ; traceTcS "simpl_loop: wc =" (ppr wc)
 
-       -- solveSimples may make progress if either float_eqs hold
        ; (unifs1, wc1) <- reportUnifications $
                           solveSimpleWanteds $
-                          floated_eqs `unionBags` simples
-            -- Notes:
-            --   - Put floated_eqs first so they get solved first
-            --     NB: the floated_eqs may include /derived/ equalities
-            --     arising from fundeps inside an implication
-
-       ; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
-       ; (no_new_scs, simples2) <- expandSuperClasses simples1
+                          simples
 
+       -- See Note [Cutting off simpl_loop]
        -- We have already tried to solve the nested implications once
        -- Try again only if we have unified some meta-variables
-       -- (which is a bit like adding more givens)
-       -- See Note [Cutting off simpl_loop]
-       ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
-                                     then return (emptyBag, implics)
-                                     else solveNestedImplications (implics `unionBags` implics1)
-
-       ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
-                    (WC { wc_simple = simples2
-                        , wc_impl   = implics2 }) }
-
-
-expandSuperClasses :: Cts -> TcS (Bool, Cts)
--- If there are any unsolved wanteds, expand one step of
--- superclasses for deriveds
--- Returned Bool is True <=> no new superclass constraints added
--- See Note [The superclass story] in TcCanonical
-expandSuperClasses unsolved
-  | not (anyBag superClassesMightHelp unsolved)
-  = return (True, unsolved)
-  | otherwise
-  = do { traceTcS "expandSuperClasses {" (ppr unsolved)
-       ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
-             get acc ct | Just ct' <- isPendingScDict ct
-                        = (ct':acc, ct')
-                        | otherwise
-                        = (acc,     ct)
-       ; pending_given <- getPendingScDicts
-       ; if null pending_given && null pending_wanted
-         then do { traceTcS "End expandSuperClasses no-op }" empty
-                 ; return (True, unsolved) }
-         else
-    do { traceTcS "expandSuperClasses mid"
-             (vcat [ text "pending_given:" <+> ppr pending_given
-                   , text "pending_wanted:" <+> ppr pending_wanted ])
-       ; new_given  <- makeSuperClasses pending_given
-       ; solveSimpleGivens new_given
-       ; new_wanted <- makeSuperClasses pending_wanted
-       ; traceTcS "End expandSuperClasses }"
-                  (vcat [ text "Given:" <+> ppr pending_given
-                        , text "Wanted:" <+> ppr new_wanted ])
-       ; return (False, unsolved' `unionBags` listToBag new_wanted) } }
+       -- (which is a bit like adding more givens), or we have some
+       -- new Given superclasses
+       ; let new_implics = wc_impl wc1
+       ; if unifs1 == 0       &&
+            no_new_given_scs  &&
+            isEmptyBag new_implics
+
+           then -- Do not even try to solve the implications
+                simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
+
+           else -- Try to solve the implications
+                do { (floated_eqs2, implics2) <- solveNestedImplications $
+                                                 implics `unionBags` new_implics
+                   ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
+    } }
 
 solveNestedImplications :: Bag Implication
                         -> TcS (Cts, Bag Implication)
@@ -1616,7 +1596,7 @@ setImplicationStatus implic@(Implic { ic_status     = status
             discard_entire_implication  -- Can we discard the entire implication?
               =  null dead_givens           -- No warning from this implication
               && not bad_telescope
-              && isEmptyBag pruned_implics  -- No live children
+              && isEmptyWC pruned_wc        -- No live children
               && isEmptyVarSet need_outer   -- No needed vars to pass up to parent
 
             final_status
diff --git a/testsuite/tests/quantified-constraints/T15290.hs b/testsuite/tests/quantified-constraints/T15290.hs
new file mode 100644 (file)
index 0000000..8a0c3d9
--- /dev/null
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290 where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+--    join = coerce
+--          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+--          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+--          join
+
+
+-- Predicative version (succeeds)
+    join = (coerce
+           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.hs b/testsuite/tests/quantified-constraints/T15290a.hs
new file mode 100644 (file)
index 0000000..bfb5b2a
--- /dev/null
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
+             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+
+module T15290a where
+
+import Prelude hiding ( Monad(..) )
+import Data.Coerce ( Coercible, coerce )
+
+class Monad m where
+  join  :: m (m a) -> m a
+
+newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
+
+newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
+
+instance Monad m => Monad (StateT s m) where
+  join = error "urk"
+
+instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
+      => Monad (IntStateT m) where
+
+--   Fails with the impredicative instantiation of coerce, succeeds without
+
+-- Impredicative version (fails)
+    join = coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a)   -> IntStateT m a)
+          join
+
+
+-- Predicative version (succeeds)
+--    join = (coerce
+--           @(StateT Int m (StateT Int m a) -> StateT Int m a)
+--           @(IntStateT m (IntStateT m a)   -> IntStateT m a)
+--           join) :: forall a. IntStateT m (IntStateT m a)   -> IntStateT m a
diff --git a/testsuite/tests/quantified-constraints/T15290a.stderr b/testsuite/tests/quantified-constraints/T15290a.stderr
new file mode 100644 (file)
index 0000000..2efd784
--- /dev/null
@@ -0,0 +1,22 @@
+
+T15290a.hs:25:12: error:
+    • Couldn't match representation of type ‘m (Int, IntStateT m a1)’
+                               with that of ‘m (Int, StateT Int m a1)’
+        arising from a use of ‘coerce’
+      NB: We cannot know what roles the parameters to ‘m’ have;
+        we must assume that the role is nominal
+    • In the expression:
+        coerce
+          @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+          @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+          join
+      In an equation for ‘join’:
+          join
+            = coerce
+                @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
+                @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
+                join
+      In the instance declaration for ‘Monad (IntStateT m)’
+    • Relevant bindings include
+        join :: IntStateT m (IntStateT m a) -> IntStateT m a
+          (bound at T15290a.hs:25:5)
index 75fcf8c..5f8547b 100644 (file)
@@ -10,3 +10,6 @@ test('T14961', normal, compile, [''])
 test('T9123a', normal, compile, [''])
 test('T15244', normal, compile, [''])
 test('T15231', normal, compile_fail, [''])
+
+test('T15290', normal, compile, [''])
+test('T15290a', normal, compile_fail, [''])