[GHC] #15347: QuantifiedConstraints: Implication constraints with type families don't work

5 Jul 2018

      #15347: QuantifiedConstraints: Implication constraints with type families don't
work
-------------------------------------+-------------------------------------
           Reporter:  aaronvargo     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This may be related to #14860, but I think it's different.

 The following code fails to compile:

 {{{#!hs
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ConstraintKinds #-}

 import Prelude()
 import Data.Kind

 data Dict c = c => Dict

 type family F a :: Constraint

 foo :: forall a b. (a => F b, a) => Dict (F b)
 foo = Dict
 }}}

 {{{
 • Could not deduce: F b arising from a use of ‘Dict’
   from the context: (a => F b, a)
 }}}

 Yet the following all do compile:

 {{{#!hs
 bar :: forall a. F a => Dict (F a)
 bar = Dict

 baz :: forall a b. (a => b, a) => Dict b
 baz = Dict

 qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
 qux = Dict
 }}}

 It seems that a wanted `F b` can be solved with a given `F b`, but not
 with a given `a => F b`, which is bizarre. The fact that `qux` still works
 is also strange, as it means that you get a different result if you first
 simplify by substituting `c = F b`.

 As a more practical example, the following similarly fails to compile, due
 to the `Cod f` type family:

 {{{#!hs
 -- in addition to the above extensions
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}

 class Ob p a

 class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
   type Dom f
   type Cod f

 liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
 liftOb = Dict
 }}}

 While a version which uses fundeps instead does compile:

 {{{#!hs
 class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom
 cod

 liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob
 cod (f a))
 liftOb = Dict
 }}}

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