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

27 Feb 2018

      #14860: QuantifiedConstraints: Can't quantify constraint involving type family
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints wipT2893     |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This program fails to typecheck using the `wip/T2893` branch, to my
 surprise:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Proxy

 type family   Apply (f :: * -> *) a
 type instance Apply Proxy a = Proxy a

 data ExTyFam f where
   MkExTyFam :: Apply f a -> ExTyFam f

 instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
   show (MkExTyFam x) = show x
   showsPrec = undefined -- Not defining these leads to the oddities
 observed in
   showList = undefined  --
 https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32

 test :: ExTyFam Proxy -> String
 test = show
 }}}

 This fails with:

 {{{
 $ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:17:24: error:
     • Could not deduce (Show (Apply f a)) arising from a use of ‘show’
       from the context: forall a. Show (Apply f a)
         bound by the instance declaration at Bug.hs:16:10-57
     • In the expression: show x
       In an equation for ‘show’: show (MkExTyFam x) = show x
       In the instance declaration for ‘Show (ExTyFam f)’
    |
 17 |   show (MkExTyFam x) = show x
    |                        ^^^^^^
 }}}

 I would have expected the `(forall a. Show (Apply f a))` quantified
 constraint to kick in, but it didn't.

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