Re: [GHC] #14860: QuantifiedConstraints: Can't quantify constraint involving type family

20 Nov 2018

      #14860: QuantifiedConstraints: Can't quantify constraint involving type family
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:  wontfix           |  QuantifiedConstraints
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 edsko):

 This is all rather unfortunate. I'd like to be able to write

 {{{#!hs
 class (forall b. Show b => Show (T a b)) => C a where
   type family T a :: * -> *

 data D a = MkD (T a Int)

 deriving instance C a => Show (D a)
 }}}

 but cannot. @simonpj writes:
...
"Remember, a quantified constraint is a bit like a local instance
 declaration. We don't allow `instance C (F a) where ...` where F is a type
 function; and no more should we allow `forall a. Show (Apply f a)` as a
 quantified constraint".
But then why can I write

 {{{#!hs
 class (Show (T a)) => C a where
   type family T a :: *

 data D a = MkD (T a)

 -- Could not deduce (Show (T a Int))
 --   arising from a use of ‘showsPrec’
 deriving instance C a => Show (D a)
 }}}

 Shouldn't by the same reasoning this fail to work also? (Please don't make
 it fail though! :-D ) (Yes, it's not quantified, but it's "trivially
 quantified"; it feels strange to me to allow one but not the other.)

 Note that for this kind of use case there is no easy workaround; as
 https://ghc.haskell.org/trac/ghc/ticket/15347#comment:15 points out, it
 involves adding new type variables to the class, kind of defeating the
 purpose of having type families in the first place. (Not to mention that I
 have a ''bunch'' of these type families in my real example.)

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