#15290 closed bug (fixed)

QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: quantified-constraints/T15290{,a,b}, deriving/should_compile/T15290{c,d}, deriving/should_compile/T14883
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4895
Wiki Page:

Description

I wanted to see if we're ready to put join into Monad. So I typed this in:

{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}

module Bug where

import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible )

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  join  :: m (m a) -> m a

newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }

instance Monad m => Monad (StateT s m) where
  ma >>= fmb = StateT $ \s -> runStateT ma s >>= \(s1, a) -> runStateT (fmb a) s1
  join ssa = StateT $ \s -> runStateT ssa s >>= \(s, sa) -> runStateT sa s

newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }

deriving instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q)) => Monad (IntStateT m)

This looks like it should be accepted. But I get

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180617 for x86_64-apple-darwin):
	addTcEvBind NoEvBindsVar
  [G] df_a67k
    = \ (@ p_a62C) (@ q_a62D) (v_B1 :: Coercible p_a62C q_a62D) ->
        coercible_sel
          @ *
          @ (m_a64Z[ssk:1] p_a62C)
          @ (m_a64Z[ssk:1] q_a62D)
          (df_a651 @ p_a62C @ q_a62D v_B1)
  a67c
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad

Change History (39)

comment:1 Changed 15 months ago by goldfire

Simpler test case:

{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving, QuantifiedConstraints #-}

module Bug where

import Data.Coerce

class C m where
  join :: m (m a) -> m a

newtype T m a = MkT (m a)

deriving instance (C m, forall p q. Coercible p q => Coercible (m p) (m q)) => C (T m)

comment:2 Changed 15 months ago by goldfire

This is blocking #9123.

comment:3 Changed 15 months ago by goldfire

Blocking: 9123 added

comment:4 Changed 15 months ago by RyanGlScott

Blocking: 14883 added

comment:5 Changed 15 months ago by simonpj

Good grief. At first I thought the problem was simple, but now I realise there is more to it than that.

Here is a minimised version that crashes

{-# 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, forall p q. Coercible p q => Coercible (m p) (m q))
      => Monad (IntStateT m) where

    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

The deriving mechanism tries to instantiate coerce at a polymorphic type, a form of impredicative polymorphism, so it's on thin ice. And in fact the ice breaks.

The call to coerce gives rise to

Coercible (forall a. blah1) (forall a. blah2)

and that soon simplifies to the implication constraint (because of the forall)

forall a <no-ev>. m (Int, IntStateT m a) ~R# m (Int, StateT Int m a)

But, becuase this constraint is under a forall, inside a type, we have to prove it without computing any term evidence. Hence the <no-ev>, meaning I can't generate any term-level evidence bindings.

Alas, I must generate a term-level evidence binding, to instantiate the quantified constraint. Currently GHC crashes, but I suppose it should instead decline to consult given quantified constraints if it's in a context where evidence bindings are not allowed. I don't see any way out here.

All this arises from a sneaky attempt to use impredicative polymorphism. Maybe instead the derviing mechansim should generate

    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

and use ordinary predicative instantiation for coerce. And indeed that works fine right now. It'll mean a bit more work for the deriving mechanism, but not much.

Richard and Ryan may want to comment.

comment:6 Changed 15 months ago by RyanGlScott

I don't think your workaround is sufficient to avoid the issue. Consider what would happen if we had a variant of join with this type signature:

join  :: (forall b. b -> a) -> m (m a) -> m a

If we plug that in to our proposed scheme:

{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
             QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}

module T15290 where

import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible, coerce )

class Monad m where
  join  :: (forall b. b -> a) -> m (m a) -> m a

newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }

instance Monad m => Monad (StateT s m) where

newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }

instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
      => Monad (IntStateT m) where

    join = coerce
          @((forall b. b -> a) -> StateT Int m (StateT Int m a) -> StateT Int m a)
          @((forall b. b -> a) -> IntStateT m (IntStateT m a)   -> IntStateT m a)
          join :: forall a. (forall b. b -> a) -> IntStateT m (IntStateT m a) -> IntStateT m a

Then that, too, will panic:

$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling T15290           ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180616 for x86_64-unknown-linux):
        addTcEvBind NoEvBindsVar
  [G] df_a1pg
    = \ (@ p_aW5) (@ q_aW6) (v_B1 :: Coercible p_aW5 q_aW6) ->
        coercible_sel
          @ *
          @ (m_a1nx[ssk:1] p_aW5)
          @ (m_a1nx[ssk:1] q_aW6)
          (df_a1nz @ p_aW5 @ q_aW6 v_B1)
  a1og
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad

comment:7 Changed 15 months ago by simonpj

Yes, I agree. I can (and will) stop the panic (by refraining from using quantified constraints if I have no place to put the evidence) but that will make GHC reject deriving for

  • A higher rank method
  • That makes essential use of a quantified constraint
  • Under a forall

I don't see how to avoid that restriction. If anyone else does, please say so!

Last edited 15 months ago by simonpj (previous) (diff)

comment:8 Changed 15 months ago by RyanGlScott

Wait, you're saying that deriving classes with methods that use higher-rank types will no longer work? If so, that is going to break enormous swaths of code both in the wild and in the test suite (see here for one example).

comment:9 Changed 15 months ago by simonpj

Wait, you're saying that deriving classes with methods that use higher-rank types will no longer work?

No, I am not saying that (see the second bullet). It's just that if you can't simultaneously exploit impredicative instantiation of coerce and quantified constraints.

comment:10 Changed 15 months ago by RyanGlScott

Ah, my apologies. I interpreted that list of bullet points as three separate criteria under which deriving would fail, not as a list of three conditions which must simultaneously hold.

In that case, I feel much better about this idea (if this really is the only way forward). I've always thought that derived instance methods should use InstanceSigs, and this gives us a good excuse to do so. (And I think certain folks, possibly from Iceland, will find that more aesthetically pleasing to look at in -ddump-deriv output.)

comment:11 Changed 15 months ago by simonpj

You could use InstanceSigs; or just an expression type signature as I have done.

And incidentally you can them omit the second type argument to coerce, which is perhaps nice.

comment:12 Changed 15 months ago by RyanGlScott

To be clear: are you working on the change to deriving alongside the typechecker changes? Or should I implement the deriving bits?

comment:13 Changed 15 months ago by simonpj

Could you do the deriving bits? Thanks!

comment:14 Changed 15 months ago by simonpj

See also #14883, which is very similar

comment:15 Changed 15 months ago by RyanGlScott

Hm, I've hit a roadblock when trying to switch over to the scheme proposed in comment:5. Consider this code:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -ddump-deriv #-}
module Bug where

import Data.Coerce

class C a where
  c :: Int -> forall b. b -> a

instance C Int where
  c _ _ = 42

newtype Age = MkAge Int

-- This is what
--
--   deriving instance C Age
--
-- would generate:
instance C Age where
  c = coerce @(   Int -> forall b. b -> Int)
             c :: Int -> forall b. b -> Age

This fails to typecheck:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:26:7: error:
    • Couldn't match representation of type ‘forall b2. b2 -> Int’
                               with that of ‘b1 -> Age’
        arising from a use of ‘coerce’
    • In the expression:
          coerce @(Int -> forall b. b -> Int) c :: Int -> forall b. b -> Age
      In an equation for ‘c’:
          c = coerce @(Int -> forall b. b -> Int) c ::
                Int -> forall b. b -> Age
      In the instance declaration for ‘C Age’
   |
26 |   c = coerce @(   Int -> forall b. b -> Int)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

The same error occurs if I use InstanceSigs.

Any ideas on how to make this work?

Last edited 15 months ago by RyanGlScott (previous) (diff)

comment:16 Changed 15 months ago by goldfire

The current behavior was introduced in b612da667fe8fa5277fc78e972a86d4b35f98364

That commit fixes some impredicativity bug but also rewrites GND to use type application. However, the change to GND also has it work with polytypes instead of its previous behavior, using monotypes. It sounds like we want to go to the previous behavior.

As for Ryan's question: try passing both type arguments to coerce. As explained in the visible type application paper, type signatures on expressions are deeply skolemized, which is causing havoc for you here. I think including the second type parameter to coerce will solve the problem.

comment:17 Changed 15 months ago by RyanGlScott

Thanks Richard, that did indeed solve that problem.

On the other hand, I seem to have hit an even trickier problem. For context: this is the entirety of my patch at the moment:

  • compiler/typecheck/TcGenDeriv.hs

    diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
    index b944520..1f1cba2 100644
    a b gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty 
    16681668                                          [] rhs_expr]
    16691669      where
    16701670        Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
     1671        (_, _, from_tau) = tcSplitSigmaTy from_ty
     1672        (_, _, to_tau)   = tcSplitSigmaTy to_ty
    16711673
    16721674        meth_RDR = getRdrName meth_id
    16731675
    16741676        rhs_expr = nlHsVar (getRdrName coerceId)
    1675                                       `nlHsAppType` from_ty
    1676                                       `nlHsAppType` to_ty
    1677                                       `nlHsApp`     nlHsVar meth_RDR
     1677                                      `nlHsAppType`     from_tau
     1678                                      `nlHsAppType`     to_tau
     1679                                      `nlHsApp`         nlHsVar meth_RDR
     1680                                      `nlExprWithTySig` to_ty
    16781681
    16791682    mk_atf_inst :: TyCon -> TcM FamInst
    16801683    mk_atf_inst fam_tc = do

i.e., drop the foralls from each of the types inside the explicit type applications, and put an explicit type signature (with foralls) on the whole expression.

Now here's the kicker: if you try that patch on this program:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -ddump-deriv #-}
module Bug where

import Data.Coerce

class Foo a where
  bar :: a -> Maybe b

instance Foo Int where
  bar _ = Nothing

newtype Age = MkAge Int
  deriving Foo

Then it no longer typechecks:

$ inplace/bin/ghc-stage2 --interactive ../Bug2.hs
GHCi, version 8.7.20180621: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( ../Bug2.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance Bug.Foo Bug.Age where
    Bug.bar
      = GHC.Prim.coerce
          @(GHC.Types.Int -> GHC.Maybe.Maybe b_a1AR)
          @(Bug.Age -> GHC.Maybe.Maybe b_a1AR)
          Bug.bar ::
          forall (b_a1AR :: TYPE GHC.Types.LiftedRep).
          Bug.Age -> GHC.Maybe.Maybe b_a1AR
  

Derived type family instances:



../Bug2.hs:16:12: error:
    • Couldn't match type ‘b1’ with ‘b’
      ‘b1’ is a rigid type variable bound by
        an expression type signature:
          forall b1. Age -> Maybe b1
        at ../Bug2.hs:16:12-14
      ‘b’ is a rigid type variable bound by
        the type signature for:
          bar :: forall b. Age -> Maybe b
        at ../Bug2.hs:16:12-14
      Expected type: Age -> Maybe b1
        Actual type: Age -> Maybe b
    • In the expression:
          coerce @(Int -> Maybe b) @(Age -> Maybe b) bar ::
            forall (b :: TYPE GHC.Types.LiftedRep). Age -> Maybe b
      In an equation for ‘bar’:
          bar
            = coerce @(Int -> Maybe b) @(Age -> Maybe b) bar ::
                forall (b :: TYPE GHC.Types.LiftedRep). Age -> Maybe b
      When typechecking the code for ‘bar’
        in a derived instance for ‘Foo Age’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘Foo Age’
    • Relevant bindings include
        bar :: Age -> Maybe b (bound at ../Bug2.hs:16:12)
   |
16 |   deriving Foo
   |            ^^^

For the life of me, I can't figure out why this shouldn't typecheck. What's even stranger, if I take the code that GHC's giving me and paste it back into the source:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -ddump-deriv #-}
module Bug where

import Data.Coerce

class Foo a where
  bar :: a -> Maybe b

instance Foo Int where
  bar _ = Nothing

newtype Age = MkAge Int
  -- deriving Foo

instance Foo Age where
  bar = coerce @(Int -> Maybe b)
               @(Age -> Maybe b)
               bar :: forall b. Age -> Maybe b

Then it typechecks again!

comment:18 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In 32eb419/ghc:

Instances in no-evidence implications

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.

comment:19 Changed 15 months ago by simonpj

Test Case: quantified-constraints/T15290, T15290a

comment:20 Changed 15 months ago by RyanGlScott

To make things more outrageous, if I manually freshen the type variable binders in to_ty in comment:17 (using freshTyVarBndrs), then it works. Quite mysterious.

comment:21 Changed 15 months ago by simonpj

I'm on it. Digging through manure in TcHsType.

comment:22 Changed 15 months ago by RyanGlScott

On the subject of the actual panic observed in this ticket, I don't think Simon's commit quite fixed it. I'm still observing the panic on commit 122ba98af22c2b016561433dfa55bbabba98d972 with this program (taken from #14883):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind

type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)

class Representational1 f => Functor' f where
  fmap' :: (a -> b) -> f a -> f b

class Functor' f => Applicative' f where
  pure'  :: a -> f a
  (<*>@) :: f (a -> b) -> f a -> f b

class Functor' t => Traversable' t where
  traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)

-- Typechecks
newtype T1 m a = MkT1 (m a) deriving (Functor', Traversable')
$ ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20180621 for x86_64-unknown-linux):
        addTcEvBind NoEvBindsVar
  [G] df_a1bF
    = \ (@ a_asM) (@ b_asN) (v_B1 :: Coercible a_asM b_asN) ->
        coercible_sel
          @ *
          @ (m_a1bn[sk:1] a_asM)
          @ (m_a1bn[sk:1] b_asN)
          (df_a1bE @ a_asM @ b_asN v_B1)
  a1bw
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcRnMonad.hs:1404:5 in ghc:TcRnMonad

The panic does not occur if I derive Traversable' through StandaloneDeriving.

comment:23 in reply to:  21 Changed 15 months ago by goldfire

Replying to simonpj:

I'm on it. Digging through manure in TcHsType.

Presumably mine. What's up this time? :)

comment:24 Changed 15 months ago by simonpj

Good grief -- again! comment:17 is ghastly. Here's what is happening. What we are 'really' checking is

  bar = ((coerce @(Int -> Maybe b)
                @(Age -> Maybe b)
                bar)
           :: forall b. Age -> Maybe b)
        :: forall b. Age -> Maybe b

where

  • the outer type signature comes from checking that the type of the method matches the type that the class expects
  • the inner one comes from the 'deriving' patch

Because both of those type sigs ultimately from the same source, both 'b's happen to have the same unique. That should be fine but it isn't:

  • The outer forall adds b :-> b1[sk] to the type environment. That's fine, even though this outer forall b does not scope; the type envt isn't responsible for resolving lexical scoping.
  • The forall on the inner signature is typechecked with by the HsForAllTy case of tc_hs_type, which calls
    • tcExplicitTKBndrs, which calls
    • tcHsTyVarBndr, which calls
    • tcHsTyVarName, which has a special case for type variables already in scope
  • The in-scope handling in tcHsTyVarName is a very special case intended only for the binders in the LHSQTyVars of an associated type or type instance declaration, nested inside a class decl. Yet it is here being used (accidentally) for the forall of a type signature, a situation that it is utterly unsuitable for. Even if the tyvar for a forall is already in scope, that should be utterly irrelevant to the type signature.
  • The net result is chaos: we end up with two different skolems that really represent the same type variable.

Conclusion: we should radically narrow the cases in which this funny in-scope test applies.

comment:25 Changed 15 months ago by RyanGlScott

Simon made a commit (9fc40c733ba8822a04bd92883801b214dee099ca) addressing the issue in comment:24, but he accidentally tagged the wrong ticket number. Here is the commit:

From 9fc40c733ba8822a04bd92883801b214dee099ca Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon, 25 Jun 2018 13:20:59 +0100
Subject: [PATCH] Refactor the kind-checking of tyvar binders

The refactoring here is driven by the ghastly mess described in
comment:24 of Trac #1520.  The overall goal is to simplify the
kind-checking of typev-variable binders, and in particular to narrow
the use of the "in-scope tyvar binder" stuff,
which is needed only for associated types: see the new
Note [Kind-checking tyvar binders for associated types] in TcHsType.

Now

* The "in-scope tyvar binder" stuff is done only in
     - kcLHsQTyVars, which is used for the LHsQTyVars of a
       data/newtype, or type family declaration.

     - tcFamTyPats, which is used for associated family instances;
       it now calls tcImplicitQTKBndrs, which in turn usese
       newFlexiKindedQTyVar

* tcExpicitTKBndrs (which is used only for function signatures,
  data con signatures, pattern synonym signatures, and expression
  type signatures) now does not go via the "in-scope tyvar binder"
  stuff at all.

While I'm still not happy with all this code, the code is generally
simpler, and I think this is a useful step forward. It does cure
the problem too.

(It's hard to trigger the problem in vanilla Haskell code, because
the renamer would normally use different names for nested binders,
so I can't offer a test.)
---
 compiler/hsSyn/HsDecls.hs          |  43 +++++--
 compiler/typecheck/TcHsType.hs     | 258 +++++++++++++++++++++----------------
 compiler/typecheck/TcTyClsDecls.hs |   3 +-
 3 files changed, 178 insertions(+), 126 deletions(-)

comment:26 Changed 15 months ago by simonpj

Thanks for putting this in the right place. I think your patch should work now; and I tried this which seems even better

diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
index b944520..736eb14 100644
--- a/compiler/typecheck/TcGenDeriv.hs
+++ b/compiler/typecheck/TcGenDeriv.hs
@@ -1668,13 +1668,12 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
                                           [] rhs_expr]
       where
         Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
-
         meth_RDR = getRdrName meth_id
+        (_, _, from_tau) = tcSplitSigmaTy from_ty
 
         rhs_expr = nlHsVar (getRdrName coerceId)
-                                      `nlHsAppType` from_ty
-                                      `nlHsAppType` to_ty
-                                      `nlHsApp`     nlHsVar meth_RDR
+                   `nlHsApp` (nlHsVar meth_RDR `nlExprWithTySig` from_tau)
+                   `nlExprWithTySig` to_ty
 
     mk_atf_inst :: TyCon -> TcM FamInst
     mk_atf_inst fam_tc = do
@@ -1703,11 +1702,6 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         rep_cvs'    = toposortTyVars rep_cvs
         pp_lhs      = ppr (mkTyConApp fam_tc rep_lhs_tys)
 
-nlHsAppType :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
-nlHsAppType e s = noLoc (HsAppType hs_ty e)
-  where
-    hs_ty = mkHsWildCardBndrs $ nlHsParTy (typeToLHsType s)
-
 nlExprWithTySig :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
 nlExprWithTySig e s = noLoc $ ExprWithTySig hs_ty
                             $ parenthesizeHsExpr sigPrec e

I like this because it feels more uniform: two type signatures rather that one type signature and two type applications.

Validate goes through (I think) except for -ddump-deriv output. Over to you on that front.

Last edited 15 months ago by simonpj (previous) (diff)

comment:27 Changed 15 months ago by RyanGlScott

Thanks, Simon.

Do be aware that the program in comment:22 still panics. I'll check that it as an expect_broken test case in my upcoming patch.

comment:28 Changed 15 months ago by simonpj

On the subject of the actual panic observed in this ticket, I don't think Simon's commit quite fixed it. I'm still observing the panic on commit 122ba98af22c2b016561433dfa55bbabba98d972 with this program (taken from #14883):

Ah, correction, I can reproduce this. Weird. I'll look.

Last edited 15 months ago by simonpj (previous) (diff)

comment:29 Changed 15 months ago by RyanGlScott

Actually, it turns out that the approach in comment:26 isn't feasible. It breaks on the program in comment:15, as it generates the following code:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module T15290b where

import Data.Coerce

class C a where
  c :: Int -> forall b. b -> a

instance C Int where
  c _ _ = 42

newtype Age = MkAge Int
  -- deriving C

instance C Age where
  c = coerce (c :: Int -> forall b. b -> Int) :: Int -> forall b. b -> Age
$ ghc Bug.hs
[1 of 1] Compiling T15290b          ( Bug.hs, Bug.o )

Bug.hs:19:7: error:
    • Couldn't match representation of type ‘b0’ with that of ‘b1’
        arising from a use of ‘coerce’
      ‘b1’ is a rigid type variable bound by
        a type expected by the context:
          Int -> forall b1. b1 -> Age
        at Bug.hs:19:50-74
    • In the expression:
          coerce (c :: Int -> forall b. b -> Int) ::
            Int -> forall b. b -> Age
      In an equation for ‘c’:
          c = coerce (c :: Int -> forall b. b -> Int) ::
                Int -> forall b. b -> Age
      In the instance declaration for ‘C Age’
   |
19 |   c = coerce (c :: Int -> forall b. b -> Int) :: Int -> forall b. b -> Age
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Since this does typecheck with the TypeApplications-based approach, I'll go with that one.

comment:30 Changed 15 months ago by simonpj

Ah, correction, I can reproduce this. Weird. I'll look.

Gah. Yet another unrelated bug, this time in TcDerivInfer.simplifyDeriv. Patch coming.

comment:31 Changed 15 months ago by RyanGlScott

Blocking: 14883 removed
Differential Rev(s): Phab:D4895
Status: newpatch

Phab:D4895 implements the deriving-related bits.

comment:32 Changed 15 months ago by simonpj

OK, this commit fixes the problem reported in comment:22, and adds the code there as a regression test.

This is the third separate bug exposed by the original bug report. Wow.

commit 261dd83cacec71edd551e9c581d05285c9ea3226
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Jun 25 17:42:57 2018 +0100

    Fix TcLevel manipulation in TcDerivInfer.simplifyDeriv
    
    The level numbers we were getting simply didn't obey the
    invariant (ImplicInv) in TcType
       Note [TcLevel and untouchable type variables]
    
    That leads to chaos. Easy to fix.  I improved the documentation.
    
    I also added an assertion in TcSimplify that checks that
    level numbers go up by 1 as we dive inside implications, so
    that we catch the problem at source rather than than through
    its obscure consequences.
    
    That in turn showed up that TcRules was also generating
    constraints that didn't obey (ImplicInv), so I fixed that too.
    I have no idea what consequences were lurking behing that
    bug, but anyway now it's fixed.  Hooray.

Are we done now? (Once Ryan has committed the stuff in comment:31.)

comment:33 in reply to:  32 Changed 15 months ago by RyanGlScott

Replying to simonpj:

Are we done now?

I certainly hope so! :) I've rebased Phab:D4895 on top of your most recent changes, so that should wrap things up on this ticket.

Another question remains of what to do with #9123, which requests that GeneralizedNewtypeDeriving emit quantified constraints involving Coercible. But this ticket shows that doing so often leads to disaster. In light of this, should we close #9123 as wontfix?

comment:34 Changed 15 months ago by simonpj

As comment:63 says (on #9123) I don't think we should ever infer quantified constraints, regardless of this ticket. So I'm fine with closing #9123

comment:35 Changed 15 months ago by bgamari

Status: patchmerge

comment:36 Changed 15 months ago by bgamari

I'm putting this in merge state since there are already a few patches that need to be backported. However, the issue here isn't quite fixed until Phab:D4895 is merged to master.

comment:37 Changed 15 months ago by Ryan Scott <ryan.gl.scott@…>

In 132273f3/ghc:

Instantiate GND bindings with an explicit type signature

Summary:
Before, we were using visible type application to apply
impredicative types to `coerce` in
`GeneralizedNewtypeDeriving`-generated bindings. This approach breaks
down when combined with `QuantifiedConstraints` in certain ways,
which #14883 and #15290 provide examples of. See
Note [GND and QuantifiedConstraints] for all the gory details.

To avoid this issue, we instead use an explicit type signature to
instantiate each GND binding, and use that to bind any type variables
that might be bound by a class method's type signature. This reduces
the need to impredicative type applications, and more importantly,
makes the programs from #14883 and #15290 work again.

Test Plan: make test TEST="T15290b T15290c T15290d T14883"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14883, #15290

Differential Revision: https://phabricator.haskell.org/D4895

comment:38 Changed 15 months ago by RyanGlScott

Blocking: 9123 removed
Test Case: quantified-constraints/T15290, T15290aquantified-constraints/T15290{,a,b}, deriving/should_compile/T15290{c,d}, deriving/should_compile/T14883

With the commit in comment:37, that should take care of business.

As far as which commits to merge, my understanding is that you would need everything mentioned in this ticket, which encompasses:

Does that sound right?

Also, I apologize in advance to Ben :)

Note: See TracTickets for help on using tickets.