Re: [GHC] #15290: QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"

21 Jun 2018

      #15290: QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:  9123, 14883
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (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:

 {{{#!diff
 diff --git a/compiler/typecheck/TcGenDeriv.hs
 b/compiler/typecheck/TcGenDeriv.hs
 index b944520..1f1cba2 100644
 --- a/compiler/typecheck/TcGenDeriv.hs
 +++ b/compiler/typecheck/TcGenDeriv.hs
 @@ -1668,13 +1668,16 @@ 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
 +        (_, _, from_tau) = tcSplitSigmaTy from_ty
 +        (_, _, to_tau)   = tcSplitSigmaTy to_ty

          meth_RDR = getRdrName meth_id

          rhs_expr = nlHsVar (getRdrName coerceId)
 -                                      `nlHsAppType` from_ty
 -                                      `nlHsAppType` to_ty
 -                                      `nlHsApp`     nlHsVar meth_RDR
 +                                      `nlHsAppType`     from_tau
 +                                      `nlHsAppType`     to_tau
 +                                      `nlHsApp`         nlHsVar meth_RDR
 +                                      `nlExprWithTySig` to_ty

      mk_atf_inst :: TyCon -> TcM FamInst
      mk_atf_inst fam_tc = do
 }}}

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

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

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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!

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15290#comment:17
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler