[GHC] #14799: QuantifiedConstraints: Problems with Typeable

12 Feb 2018

      #14799: QuantifiedConstraints: Problems with Typeable
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints, wipT2893    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This compiles

 {{{#!hs
 {-# Language GADTs, ConstraintKinds, ScopedTypeVariables,
 QuantifiedConstraints #-}

 import Data.Typeable

 data Ex cls where
   MkEx :: cls xx => xx -> Ex cls

 a :: Ex Typeable -> TypeRep
 a (MkEx (_::xx)) = typeRep @_ @xx Proxy

 -- b :: (forall xx. cls xx => Typeable xx) => Ex cls -> TypeRep
 -- b (MkEx (_::xx)) = typeRep @_ @xx Proxy

 c :: (forall xx. cls xx => Show xx) => Ex cls -> String
 c (MkEx xx) = show xx
 }}}

 but uncommenting `b` is too much:

 {{{
 $ qc hs/189-bug.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( hs/189-bug.hs, interpreted )

 hs/189-bug.hs:12:20: error:
     • Could not deduce (Typeable xx) arising from a use of ‘typeRep’
       from the context: forall xx. cls xx => Typeable xx
         bound by the type signature for:
                    b :: forall (cls :: * -> Constraint).
                         (forall xx. cls xx => Typeable xx) =>
                         Ex cls -> TypeRep
         at hs/189-bug.hs:11:1-60
       or from: cls xx
         bound by a pattern with constructor:
                    MkEx :: forall xx (cls :: * -> Constraint). cls xx =>
 xx -> Ex cls,
                  in an equation for ‘b’
         at hs/189-bug.hs:12:4-15
     • In the expression: typeRep @_ @xx Proxy
       In an equation for ‘b’: b (MkEx (_ :: xx)) = typeRep @_ @xx Proxy
    |
 12 | b (MkEx (_::xx)) = typeRep @_ @xx Proxy
    |                    ^^^^^^^^^^^^^^^^^^^^
 Failed, no modules loaded.
 Prelude>
 }}}

 This is maybe because of the `Typeable` solver.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14799
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler