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. |
13 | | |
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). |
15 | | |
16 | | * The current implementation considers coincident overlap among equations within an instance group when matching. See below for more info. |
17 | | |
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 ([http://www.cis.upenn.edu/~eir Richard]) think we should work to lift this restriction, taking Chak's points into consideration. For example, the following is tantalizing: |
19 | | {{{ |
20 | | type instance Plus n m 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) |
25 | | }}} |
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? |
27 | | |
28 | | == Coincident overlap within a branched instance == |
| 12 | == Coincident overlap within a closed type family == |
44 | | According to the [wiki:NewAxioms main page] about branched instances, "We only match a type against an equation in an instance group when no previous equation can unify against the type." Unfortunately, that kills us here. Consider reducing {{{And f True}}}. The first three branches clearly don't match. The fourth matches. But, the first two branches unify (i.e., they might apply later, depending on the instantiation for {{{f}}}), so we're stuck. Instead, we propose to scan through the branched instances at the declaration, and look to find only problematic orderings. In the declaration above, there are no problematic orderings -- if a previous branch might apply later, we'd get the same result anyway, so we're OK. Then, during matching, we only check problematic previous branches. |
| 27 | According to the [wiki:NewAxioms main page] about closed type families, "We only match a type against an equation in a closed type family when no previous equation can unify against the type." Unfortunately, that kills us here. Consider reducing {{{And f True}}}. The first three branches clearly don't match. The fourth matches. But, the first two branches unify (i.e., they might apply later, depending on the instantiation for {{{f}}}), so we're stuck. Instead, we scan through the equations at the declaration and look to find compatible equations. Two equations are compatible if their right-hand sides match whenever their left-hand sides do. In the declaration above, all equations are compatible -- if a previous equation might apply later, we'd get the same result anyway, so we're OK. Then, during matching, we only check ''in''compatible previous equations. |
55 | | The only problematic ordering is {{{F Bool}}} before {{{F a}}}. Why? Let's consider this piece by piece. {{{F Int}}} can have no problematic previous branches, because it has no previous branches. A use site that matches {{{F Bool}}} will never later match {{{F Int}}}, {{{F Int}}} is not a problematic previous branch of {{{F Bool}}}. {{{F Int}}} might later match something that matches {{{F a}}}, but the right-hand sides coincide, so {{{F Int}}} is not problematic here either. On the other hand, {{{F Bool}}} might also later match something that matches {{{F a}}} and the right-hand sides ''don't'' coincide, so {{{F Bool}}} ''is'' problematic. The upshot is that, if {{{F a}}} matches a use site, we have to make sure that {{{F Bool}}} cannot later apply. Otherwise, we can skip that check. |
| 38 | The only incompatible pair of equations is {{{F Bool}}} and {{{F a}}}. Why? Let's consider this piece by piece. A use site that matches {{{F Bool}}} will never later match {{{F Int}}}, so {{{F Int}}} is compatible with {{{F Bool}}}. {{{F Int}}} might later match something that matches {{{F a}}}, but the right-hand sides coincide, so these equations are compatible. On the other hand, {{{F Bool}}} might also later match something that matches {{{F a}}} and the right-hand sides ''don't'' coincide, so these equations are not compatible. The upshot is that, if {{{F a}}} matches a use site, we have to make sure that {{{F Bool}}} cannot later apply. Otherwise, we can skip that check. |