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

27 Jul 2018

      ...
The superclass isn't allowed to mention variables which don't appear in
#15347: QuantifiedConstraints: Implication constraints with type families don't
work
-------------------------------------+-------------------------------------
        Reporter:  aaronvargo        |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:                    |  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 simonpj):

 the head,

 Ah, I was thinking "instance decl" but actually we have a class decl.  My
 mistake.

 Not allowing functions in the instance head not to do with ''ambiguity'';
 it's to do with ''coherence'.  Consider, at the term level
 {{{
 f [x]           = x-1
 f (reverse [x]) = x+1
 }}}
 `reverse` is perfectly injective, but we don't want `(f e)` to return
 different answers depending on the evaluated-ness of `e`.

 Can you distil a small example that shows the utility of having a function
 in the head?

 -------------
 Guessing, maybe what you want is this:
 {{{
 class (forall a. Eq a => Eq (F t a)) => C t where
   type F t :: * -> *

 instance C Int where
   F Int = Maybe

 f1 :: C t => ...
 f1 = e1

 f2 :: C Int => ...
 f2 = e2
 }}}
 In `f1` we have the quantified constraint available but with a function in
 the head, so it's unusuable.  But in `f2` the quantified constraint
 becomes
 {{{
 forall a. Eq a => Eq (F Int a)
 }}}
 which rewrites (via the type instance) to
 {{{
 forall a. Eq a => Eq (Maybe a)
 }}}
 and this ''is'' usable.

 So, maybe a quantified constraints with a function in the head is just
 "parked", but it wakes up if the function can be reduced.

 This all seems complicated to specify, let alone implement, but it's the
 closest I can get.

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