38 | | * (B) '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' |
39 | | Remember "unification succeeds" means "overlap detected", so (B) is a bit more permissive than (A). For example |
| 38 | * (B) '''when performing the overlap check, allow two types to overlap even if only infinite types would witness the overlap''' |
| 39 | The idea here is that our root problem comes from a combination of nonlinearity and infinite types. So, simply make the overlap checker consider the possibility of types that contain themselves (the only possible form of infinite types). |
| 40 | (B) is a bit more permissive than (A). For example |
46 | | Intuition: under (B) the only way that unification fails is because of a definite conflict (eg `Int` ~ `Bool`). And unification failing is what allows us to accept the two equations as non-overlapping. So if we accept them, they have a definite conflict. |
| 47 | Intuition: under (B) the only way that two types don't overlap is because of a definite conflict (eg `Int` ~ `Bool`). |
| 48 | |
| 49 | How to implement (B)? It may be as easy as omitting the occurs check during unification. The way GHC detects overlap is by trying to unify the left-hand sides of two instances. If they can unify, then they overlap. Currently (GHC 7.6.3), unification fails for the two instances for `F` above, so they don't overlap. The unification fails because of the so-called "occurs check": when we are unifying a type variable (say, `x`) against a non-type-variable, (say `[x]`), we check to make sure that the type variable does not appear anywhere within the non-type-variable. (If the variable does appear in the other type, then the substitution has no fixpoint.) We could simply turn this check off, in this particular case. The net effect is to consider the possibility of infinite types. |
| 50 | |
| 51 | But, it just might not be so easy. What, exactly, should the unification algorithm do when the occurs check notes an occurrence in this case? Normally, the algorithm builds a substitution, but that would be impossible here. Yet, we need to record ''something'' about what we've discovered. For example, take this: |
| 52 | |
| 53 | {{{ |
| 54 | type family NotSure x y |
| 55 | type instance NotSure x x = Int |
| 56 | type instance NotSure [x] (Maybe x) = Bool |
| 57 | }}} |
| 58 | |
| 59 | It seems that these do not overlap, even in the presence of infinite types. But, a naive omission of the occurs check might say that these types do overlap. Getting this case wrong isn't terrible, but it would be nice to get it right. (Note that we would end up too conservative, which is OK in this case.) |
59 | | However, the above proposal of linearizing the LHS before checking overlap makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. '''So the proposal abandons support for coincident overlap between standalone type instances'''. (It's worth noting, though, that there is already no support for coincident overlap between branched type instances, or between a singleton type instance and a branched one; it is currently only supported between singleton type instances.) |
| 72 | However, the above proposal of linearizing the LHS before checking overlap (plan (A)) makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. '''So the proposal abandons support for coincident overlap between standalone type instances'''. (It's worth noting, though, that there is already no support for coincident overlap between branched type instances, or between a singleton type instance and a branched one; it is currently only supported between singleton type instances.) |
| 73 | |
| 74 | Plan (B) above has a better relationship with coincident overlap, but not quite a rosy one: in the event that an infinite type is needed to show the overlap, we don't have a well-defined substitution to apply to the RHS. It is conceivable to allow coincident overlap only when the unification algorithm produces a bona fide substitution. But, there may be no need for this. |
63 | | |
64 | | == Problem: branched instances == |
65 | | |
66 | | But, how does this interact with branched instances (those new instance forms that allow for ordered overlapping)? We still need nonlinear branched instances, as the canonical example of a nonlinear instance is an equality test: |
67 | | {{{ |
68 | | type family Equals a b :: Bool |
69 | | |
70 | | type instance where |
71 | | Equals x x = True |
72 | | Equals x y = False |
73 | | }}} |
74 | | ... |
75 | | |
76 | | The solution is to declare a ''type space'' that all branches fit within. |
77 | | |
78 | | For example: |
79 | | {{{ |
80 | | type family Equals a b :: Bool |
81 | | |
82 | | type instance Equals x y where |
83 | | Equals x x = True |
84 | | Equals x y = False |
85 | | }}} |
86 | | The header "`type instance Equals x y`" declares the "type space" of the declaration; the `where` part says how to match calls within that type space (top to bottom). |
87 | | |
88 | | In this case the type space is the whole space, but that need not be the case: |
89 | | {{{ |
90 | | type family F a b :: * |
91 | | |
92 | | type instance F Int x where |
93 | | F Int Bool = Double |
94 | | F Int Int = Char |
95 | | F Int a = Bool |
96 | | |
97 | | type instance F Bool y = Int |
98 | | }}} |
99 | | Here the first `type instance` covers calls of form `(F Int x)`, while the second covers |
100 | | calls of form `(F Bool y)`. |
101 | | |
102 | | All the equations in the `where` part must be part of (i.e. an instance of) the |
103 | | type space declared in the header. For example, this will be disallowed: |
104 | | |
105 | | {{{ |
106 | | type instance Bad [x] y where |
107 | | Bad [Int] Int = Bool -- OK |
108 | | Bad a b = () -- not OK: outside the type space (Bad [x] y) |
109 | | }}} |
110 | | |
111 | | The declared type space will be checked for overlap with other instances using the same linearization check that unbranched instances use. |
112 | | |
121 | | * Optional: Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space. [wiki:NewAxioms/TypeSpaces This page] has the details. |
122 | | |
123 | | * Optional: Add new syntax {{{type family Foo a b where { Foo ... = ... ; Foo ... = ... } }}} to declare a type family with one branched instance covering the entire type space. This would be a ''closed'' type family. |
124 | | |
125 | | == Discussion about coincident overlap == |
126 | | |
127 | | This proposal has the net effect of forcing all uses of coincident overlap to appear in one module, instead of spread across modules. That's admittedly not great, but it's possible that no one will be negatively affected. The only alternative we've (Simon, Dimitrios, Richard) thought of is to disallow coincident overlap when the left-hand sides are non-linear, but that seems very ugly and ad-hoc. |
128 | | |
129 | | To see why disallowing coincident overlap checking for unbranched axioms is vitally necessary, consider this example: |
130 | | |
131 | | {{{ |
132 | | type instance F a a Int = a |
133 | | type instance F c d d = Int |
134 | | }}} |
135 | | |
136 | | This overlap is most certainly are not OK (think about {{{F G G G}}}, where this is the malignant {{{G}}} from the beginning of this page), but they do coincide in the region of overlap. Yuck Yuck! So, we give up and just say "no" to coincident overlap in this case. |
| 86 | * Optional: Change the syntax for branched family instances, as described [wiki:NewAxioms/ClosedTypeFamilies here]. |