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 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.

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