[GHC] #15351: QuantifiedConstraints ignore FunctionalDependencies

[GHC]

#15351: QuantifiedConstraints ignore FunctionalDependencies
-------------------------------------+-------------------------------------
        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 AntC):

 Replying to [comment:6 simonpj]:
 > Yes, you are right.

 Sorry to be dumb, but who is 'you' and which bit are they 'right' about?

 > It's worth reading the original paper

 Yes I've pored over both your 2000 paper with Ralf, and the hs 2017 more
 detailed logic. (Both linked from the github proposal.) I didn't see any
 examples without a `=>` implication; I didn't see any examples without any
 instances declared at all. And the github proposal didn't mention such
 possibilities either.

 > It's intriguing -- I never expected people to explore the outer limits
 of quantified constraints so rapidly. I hope that means that they are
 proving useful (when not so close to the limits).  Is that so?

 I think this extension is going to be huge -- and that was assuming the
 implications are needed. Experiments I will try when I get my hands on it:

 * subsuming quasi-injective logic

 {{{
 class ( (b1 ~ True, b2 ~ True)   => res ~ True,
         res ~ True               => b1 ~ True,
         res ~ True               => b2 ~ True,
         (res ~ False, b1 ~ True) => b2 ~ False,
         (res ~ False, b2 ~ True) => b1 ~ False )
       => And (b1 :: Bool) (b2 :: Bool) ( res :: Bool)
 }}}

 * subsuming FunDeps

 {{{
 class (forall b'. C a b' => b' ~ b)     -- replicates GHC's "bogus" FD
 consistency check ref Trac #10675
       => C a b  where ...               -- don't need | a -> b
 }}}

   (Is there any way to get a 'strict' after substitution `b'` equal type
 `b` consistency check?)

 * maybe subsuming overlap logic/apartness guards (of course more
 interesting uses than this example)

 {{{
 class ( e ~ e' => d ~ Z, e /~ e' => d ~ (S d'), FindElem e l' d')
       => FindElemPosn e '( e'  ': l' ) (d :: Nat)  where ...
 }}}

 * field presence/absence for record extension/projection

 {{{
 class ( (forall l a. HasField r1 l a                        => HasField r3
 l a),
         (forall l a. HasField r2 l a                        => HasField r3
 l a) )
       => Merge r1 r2 r3
 class ( (forall l a. HasField r3 l a                        => HasField r1
 l a),
         (forall l a a'. (HasField r1 l a, HasField r2 l a') => HasField r3
 l a),
         (forall l. Lacks r2 l                               => Lacks r3 l)
 )
       => Project r1 r2 r3
 }}}

 (Apologies for poaching on @aaron's ticket: you're welcome to try the
 above ideas.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler