[GHC] #11534: Allow class associated types to reference functional dependencies

[GHC]

#11534: Allow class associated types to reference functional dependencies
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  FunctionalDependencies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to Simon:

 > This would make it possible for given constraints involving fundeps to
 work properly, which they don't at present (as ​Iavor points out).

 Iavor is mostly complaining that currently you can declare instances that
 break FunDeps Consistency. (And because GHC knows that, it is conservative
 in applying type improvement via FunDeps. Also his examples either break
 the FunDeps Coverage Condition -- so needing `UndecidableInstances`; or
 use dependents (rhs of FunDeps arrow) with no free vars, so there's no
 algorithmic determinism.)

 If we desugar FunDeps to Type Families, and allow them to be Closed Type
 Families, then we can carry on breaking FunDeps Consistency, via
 overlapping equations.

 If OTOH we desugar FunDeps to Open Type Families, then we can't write
 overlapping equations; therefore we can't define (for example) a type-
 level Type Equality test. (This is somewhat orthogonal to whether we can
 write overlapping instances for the Class.)

 I can see the combination of FunDeps and `OverlappingInstances` is deadly
 for consistency. (To be precise, overlap of the determinants for FunDeps,
 on lhs of the arrow.) I can also see how terrifically useful it is -- for
 example for all sorts of record-like systems from HList onwards.

 I think I could make an argument that actually the combo
 FunDeps+Overlapping is consistent. That would need going back to the
 database Relational Theory from which Mark Jones borrowed FunDeps. And
 would require some discipline in what instances you declare. (I think most
 people actually observe that discipline, but GHC doesn't enforce it. I
 have an idea how we could help GHC enforce it -- a very old, recycled idea
 from Tom Schrijvers/CHRs.)

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