Changes between Initial Version and Version 1 of NewAxioms/CoincidentOverlap

Aug 21, 2012 2:17:42 AM (5 years ago)



  • NewAxioms/CoincidentOverlap

    v1 v1  
     1= Overlapping Type Family Instances with Coincident Right-Hand Sides =
     3In the official release of GHC, it is permitted to write something like this:
     6type instance F Int = Int
     7type instance F a   = a
     10These instances surely overlap, but in the case when they do, the right-hand sides coincide. This page explores the design space around this feature with an eye toward adding instance groups, as discussed [wiki:NewAxioms here].
     12 * In the current (Aug 2012) implementation of family instance groups, no overlap (even coincident) overlap is allowed between a group and another instance. It may be possible to change the implementation to allow such overlap, but it adds another layer of complexity to the GHC code and may not be worth it. Add comments if you have a good use case for why we need coincident overlap involving an instance group.
     14 * The current implementation retains the ability for coincident overlap among non-group instances, for backward compatibility (and because this case is not hard to implement).
     16 * The current implementation considers coincident overlap among equations within an instance group when matching. See the implementation notes [wiki:NewAxioms here] for more info.
     18 * Coincident overlap (both between single instances and within an instance group) requires syntactic equality after expansion of vanilla type synonyms. In particular, type families are not expanded. Chak defends this design decision in the comments of #4259; that bug report is a request to lift this restriction. I ([ Richard]) think we should work to lift this restriction, taking Chak's points into consideration. For example, the following is tantalizing:
     20type instance where
     21  Plus Zero     n        = n
     22  Plus (Succ m) n        = Succ (Plus m n)
     23  Plus m        Zero     = m
     24  Plus m        (Succ n) = Succ (Plus m n)
     26  Figuring out that the right-hand sides are confluent requires expanding the {{{Plus}}} type family one time. What do you think? Would this be useful?