Re: [GHC] #14883: QuantifiedConstraints don't kick in when used in TypeApplications

7 Mar 2018

      #14883: QuantifiedConstraints don't kick in when used in TypeApplications
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:                    |  QuantifiedConstraints, wipT2893
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Here's a simpler version of the original program, if `Traversable` is too
 dense:

 {{{#!hs
 {-# 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 Distributive g where
   distribute :: Representational1 f => f (g a) -> g (f a)

 -- Typechecks
 newtype T1 g a = MkT1 (g a)
 instance Distributive g => Distributive (T1 g) where
   distribute :: forall f a. Representational1 f => f (T1 g a) -> T1 g (f
 a)
   distribute = coerce @(f    (g a) ->    g (f a))
                       @(f (T1 g a) -> T1 g (f a))
                       distribute

 -- Doesn't typecheck
 newtype T2 g a = MkT2 (g a)
 instance Distributive g => Distributive (T2 g) where
   distribute = coerce @(forall f a. Representational1 f => f    (g a) ->
 g (f a))
                       @(forall f a. Representational1 f => f (T2 g a) ->
 T2 g (f a))
                       distribute
 }}}

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