GHC: Ticket #4259: Relax restrictions on type family instance overlap
http://ghc.haskell.org/trac/ghc/ticket/4259
<p>
The following reduced fragment of some real code is rejected, but could be accepted, by GHC:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (f a) (f b) = LessEq a b
</pre><p>
GHC says:
</p>
<pre class="wiki"> Conflicting family instance declarations:
type instance LessEq a a
-- Defined at /home/richards/.random/tf.hs:5:14-19
type instance LessEq (f a) (f b)
-- Defined at /home/richards/.random/tf.hs:6:14-19
</pre><p>
This is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of -XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.
</p>
<p>
In particular (absent -XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.
</p>
<p>
In order to retain soundness in the presence of -XUndecidableInstances, any pair of type instances, where either instance could not be compiled without -XUndecidableInstances, would continue to use the current syntactic equality rule.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/4259
Trac 1.0.7simonpjThu, 19 Aug 2010 07:45:45 GMTsummary changed; blockedby set
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:1
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:1
<ul>
<li><strong>blockedby</strong>
set to <em>4232</em>
</li>
<li><strong>summary</strong>
changed from <em>Type family instance conflict checks could be smarter</em> to <em>Add overlapping instances for type families</em>
</li>
</ul>
<p>
If I'm getting this right, overlap is OK if, <strong>but only if</strong>, the overlapping instances are all declared in the same module. If they come in different modules there's a danger that the type checker will rewrite <tt>(F [Int])</tt> to <tt>Bool</tt> in one place, and to <tt>Char</tt> in another, and that's unsound. This is to do with soundness, not termination.
</p>
<p>
We have not implemented the "overlap ok within one module" feature yet. So it's a feature request, but it's one that I think will be popular. We'll look at it after the new type checker is working.
</p>
TicketlilacThu, 19 Aug 2010 10:45:15 GMTsummary changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:2
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:2
<ul>
<li><strong>summary</strong>
changed from <em>Add overlapping instances for type families</em> to <em>Relax restrictions on type family instance overlap</em>
</li>
</ul>
<p>
I don't think that's an accurate summary. Section 7.7.2.2.2 of the <a href="http://www.haskell.org/ghc/docs/6.12.1/html/users_guide/type-families.html">user's guide</a> says:
</p>
<p>
"The instance declarations of a type family used in a single program may only overlap if the right-hand sides of the overlapping instances coincide for the overlapping types. More formally, two instance declarations overlap if there is a substitution that makes the left-hand sides of the instances syntactically the same. Whenever that is the case, the right-hand sides of the instances must also be syntactically equal under the same substitution."
</p>
<p>
And indeed that is the case. The following code is accepted by GHC 6.12 today:
</p>
<pre class="wiki">module Tf1 where
type family Foo a :: *
module Tf2 where
import Tf1
type instance Foo (Int, a) = a
module Tf3 where
import Tf1
type instance Foo (a, Int) = a
module Tf4 where
import Tf1
import Tf2
import Tf3
a :: Foo (Int, Int)
a = 0
</pre><p>
So, type family instance overlap is /already/ permitted (and permitted by default, even). However, in order to ensure soundness, GHC applies the rule that any overlapping type family instances must have structurally equal RHSs once the LHSs are unified. It's that rule that I would like generalized (and generalized globally, not just within the scope of one module). The generalization I'd like is that the RHSs be equal after expanding all expandable type family instances and type synonyms.
</p>
<p>
The summary contains a sketch proof that this retains soundness. However, that proof relies on all type family applications on the RHS of the type family instance being smaller than the instance head (I'm not sure if soundness is violated if this restriction is dropped, but termination of the check certainly is). Therefore I suggest that the overlap soundness checking for instances which contain non-smaller instance applications on the RHS (that is, those which would not be accepted without -XUndecidableInstances) use a structural equality check; this seems like a reasonable tradeoff to me.
</p>
<p>
[Incidentally, I think the currently-implemented overlap check may be unsound in the presence of dynamically-loaded code: it assumes that there exists a module from which all type family instances used by the program are visible.]
</p>
TicketchakFri, 20 Aug 2010 02:10:09 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:3
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:3
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4259#comment:2" title="Comment 2">lilac</a>:
</p>
<blockquote class="citation">
<p>
So, type family instance overlap is /already/ permitted (and permitted by default, even). However, in order to ensure soundness, GHC applies the rule that any overlapping type family instances must have structurally equal RHSs once the LHSs are unified. It's that rule that I would like generalized (and generalized globally, not just within the scope of one module). The generalization I'd like is that the RHSs be equal after expanding all expandable type family instances and type synonyms.
</p>
</blockquote>
<p>
I explicitly decided against this when implementing type families for two reasons. Firstly, it is confusing as whether a family instance is accepted or not depends on the currently visible instances of other type families. That leads to fragile code. (More over using different rules depending on whether UndecidableInstances are allowed is confusing, too.)
</p>
<p>
Secondly, implementing such a relaxed check seems very complicated to me; especially in the presence of mutually recursive family declarations. In particular, you can get into a situation where you need to use a type family for expansion that you haven't checked for overlap yet. Combine this with the already elaborate system to make the overlap check efficient in the presence of incrementally loaded modules and orphan instances, and this will get rather complicated. (Given the concerns about mutually recursive definitions, I wouldn't even consider implementing it without properly formalising the checking procedure and rigorous proof of its termination.)
</p>
TicketsimonpjFri, 20 Aug 2010 06:46:21 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:4
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:4
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> added
</li>
</ul>
<p>
I agree with Manuel points, but I can see the attraction of Lilac's suggestion. Leaving aside the exact rules, the point is that the rules for <tt>LessEq</tt> <em>are</em> confluent, even though more than one may apply. I wonder whether this is an unusual example, or whether there are many like it?
</p>
<p>
Beyond that, I think it's true that one can have two overlapping instances, even if their RHSs are entirely different, provided they are given together. Thus
</p>
<pre class="wiki">type family F a
type instance F [a] = Bool
type instance F [Int] = Char
</pre><p>
Now, the term <tt>F [Char]</tt> is unambiguously equal to <tt>Bool</tt>. But <tt>F [b]</tt> can't reduce, because we don't know what <tt>b</tt> will be instantiated to.
</p>
<p>
On reflection though, I was too hasty in making this suggestion yesterday. It might be fine for a <em>source</em> language, but I'm not sure how to express it in System FC, the <em>intermediate</em> language. If we have the above two rules as axioms we could just compose them in sequence to get <tt>Bool ~ Char</tt> which is obvious nonsense. The only decent approach I can see is for the first rule to take a proof that <tt>a</tt> is <em>not</em> <tt>Int</tt>, and that seems pretty complicated.
</p>
<p>
So I'm not sure of the best way to proceed here.
</p>
<p>
Simon
</p>
TicketchakFri, 20 Aug 2010 11:22:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:5
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:5
<p>
We are always going to miss out on some systems that are, in fact, confluent. IIRC we don't know whether the system is terminating before we know whether it is confluent. Hence, a general check for confluence for family instances is undecidable. All that we can hope to achieve is a conservative syntactic criterion that ensures confluence (and hence indirectly, termination). I chose the currently implemented criterion because it is simple (as in, easily explained) and can be implemented efficiently in the context of separate compilation.
</p>
<p>
Maybe there is a more permissive syntactic criterion that we can use, but I believe it must be simple (and hence, not fragile) and we need to make sure we can implement it efficiently in an incremental fashion (due to the incremental loading of modules, and hence, extension of the rule set).
</p>
TicketlilacFri, 20 Aug 2010 13:35:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:6
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:6
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4259#comment:3" title="Comment 3">chak</a>:
</p>
<blockquote class="citation">
<p>
Firstly, it is confusing as whether a family instance is accepted or not depends on the currently visible instances of other type families. That leads to fragile code.
</p>
</blockquote>
<p>
That is already the case for entities other than type family instances. For instance, in this code:
</p>
<pre class="wiki">class Foo a where f :: a -> a
instance Foo Int where f = id
type family Bar a :: *
g a = f (a :: Bar Int)
</pre><p>
If "type instance Bar Int = Int" is also visible, this code compiles. Otherwise, it does not.
</p>
<p>
Further, if adding an import provides an instance which allows overlap soundness checking to succeed, then I believe that instance must be an orphan. I think issues with missing imports of orphan instances are reasonably well understood by the Haskell community.
</p>
<p>
Finally, I'd argue that the currently-implemented check is fragile. If I refactor a type family instance to an equivalent instance (for instance, by manually expanding or unexpanding a type family application on the RHS), my code (or maybe someone else's code) stops compiling. With my proposed check, that simply cannot happen, if you don't use the uncommon and unsafe extension UndecidableInstances (it is already the case that correct refactorings with that extension enabled can cause compilation failures/nontermination, so this is nothing new).
</p>
<blockquote class="citation">
<p>
(More over using different rules depending on whether UndecidableInstances are allowed is confusing, too.)
</p>
</blockquote>
<p>
Strictly, it's not a question of whether they're allowed, but whether they're actually used for a given instance. Turning on UndecidableInstances would not cause any programs to fail the soundness check which otherwise have passed it. My personal view is that this shouldn't be an issue, if documented clearly:
</p>
<p>
"Type family applications which are no smaller than the instances being checked are not expanded, even if UndecidableInstances is enabled. This condition is independent of whether the type family is associated or not, and it is not only a matter of termination, but one of type safety."
</p>
<blockquote class="citation">
<p>
Secondly, implementing such a relaxed check seems very complicated to me; especially in the presence of mutually recursive family declarations. In particular, you can get into a situation where you need to use a type family for expansion that you haven't checked for overlap yet.
</p>
</blockquote>
<p>
I know basically nothing about the implementation, so I can't really make a useful comment on implementation difficulties. However, I did consider the algorithmic complexity of the check when formulating my suggestion, and my 10,000ft view was that it shouldn't be a problem, because:
</p>
<p>
In such cases, you can use any of the (overlapping) instances which applies; the check is still sound, due to the size-based ordering. (That is, you can assume all smaller type family applications are sound when performing soundness checking on a pair of instances, even if you've not checked those smaller rules yet). The check does not need to recursively invoke itself.
</p>
<p>
Regarding simonpj's suggestion of allowing even unsound overlap (with an implicit top-to-bottom priority ordering) within a module, that would certainly solve my immediate problem (but it does damage the story for open type families somewhat). The discussion <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies"><span class="icon"></span>here</a> seems very relevant. However, I think that is an orthogonal issue -- relaxing the overlap restrictions would still have value even with that suggestion in place.
</p>
TicketiglooSat, 18 Sep 2010 13:30:48 GMTblockedby deleted
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:7
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:7
<ul>
<li><strong>blockedby</strong>
<em>4232</em> deleted
</li>
</ul>
TicketiglooThu, 30 Sep 2010 18:41:14 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:8
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:8
<ul>
<li><strong>milestone</strong>
set to <em>7.0.1</em>
</li>
</ul>
TicketsimonpjWed, 15 Dec 2010 16:53:04 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:9
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:9
<ul>
<li><strong>milestone</strong>
changed from <em>7.0.1</em> to <em>7.2.1</em>
</li>
</ul>
<p>
We clearly aren't going to do this in 7.0, so re-milestoning.
</p>
TicketbasvandijkWed, 09 Nov 2011 13:50:12 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:10
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:10
<ul>
<li><strong>cc</strong>
<em>v.dijk.bas@…</em> added
</li>
</ul>
TicketbasvandijkWed, 09 Nov 2011 14:42:32 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:11
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:11
<p>
I would like to give another use-case for overlapping type family instances:
</p>
<p>
As explained in ticket <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5595" title="bug: Unification under a forall doesn't allow full constraint solving (closed: fixed)">#5595</a> I'm giving <tt>monad-control</tt> <a class="ext-link" href="https://github.com/basvandijk/monad-control/blob/master/Control/Monad/Trans/Control.hs"><span class="icon"></span>a new design</a>.
</p>
<p>
My <a class="ext-link" href="http://hackage.haskell.org/package/regions"><span class="icon"></span>regions</a> package uses <tt>monad-control</tt> so I'm now adapting that package to the new design. However I'm stuck because I can't use an overlapped instance of an associated data type. First some background:
</p>
<p>
For <a class="ext-link" href="https://github.com/basvandijk/regions/wiki/unsafeLiftControlIO"><span class="icon"></span>safety-reasons</a> I don't want to make <tt>RegionT</tt> an instance of <tt>MonadControlIO</tt>. However I do need the ability to lift control operators like <tt>bracket</tt> or <tt>alloca</tt> into regions.
</p>
<p>
So what I did is, I created a class which is isomorphic to <tt>MonadControlIO</tt> called <a class="ext-link" href="http://hackage.haskell.org/packages/archive/regions/0.11/doc/html/Control-Monad-Trans-Region.html#t:RegionControlIO"><span class="icon"></span>RegionControlIO</a>. Just like <tt>MonadControlIO</tt> has the method <tt>liftControlIO</tt>, this class has the method <a class="ext-link" href="http://hackage.haskell.org/packages/archive/regions/0.11/doc/html/Control-Monad-Trans-Region-Unsafe.html#v:unsafeLiftControlIO"><span class="icon"></span>unsafeLiftControlIO</a>. This method however is only exported from the <tt>Unsafe</tt> module. So users are warned when using it. (I plan to use <tt>SafeHaskell</tt> to formalize this)
</p>
<p>
I made <tt>RegionT</tt> an instance of <tt>RegionControlIO</tt>:
</p>
<pre class="wiki">instance RegionControlIO pr ⇒ RegionControlIO (RegionT s pr) where
unsafeLiftControlIO f = ...
</pre><p>
Besides that I added a catch-all instance:
</p>
<pre class="wiki">{-# LANGUAGE OverlappingInstances #-}
instance MonadControlIO m ⇒ RegionControlIO m where
unsafeLiftControlIO = liftControlIO
</pre><p>
These two instances allows you to lift control operators into a stack of regions with an arbitrary stack of monad transformers at its base. For example: <tt>RegionT s1 (RegionT s2 (RegionT s3 (StateT Int (WriterT String IO))))</tt>
</p>
<p>
Now back to the problem. As said, I'm adapting <tt>regions</tt> to use the new design of <tt>monad-control</tt>. The <tt>RegionControlIO</tt> type class now looks like this:
</p>
<pre class="wiki">class MonadIO m ⇒ RegionControlIO m where
data RegionStIO m ∷ * → *
unsafeLiftControlIO ∷ (RegionRunInIO m → IO α) → m α
unsafeRestore ∷ RegionStIO m α → m α
type RegionRunInIO m = ∀ β. m β → IO (RegionStIO m β)
</pre><p>
regions are again made an instance of this type class:
</p>
<pre class="wiki">instance RegionControlIO pr ⇒ RegionControlIO (RegionT s pr) where
newtype RegionStIO (RegionT s pr) α = StIOR (RegionStIO pr ... α))
unsafeLiftControlIO f = ...
unsafeRestore (StIOR stIO) = ...
</pre><p>
As before, I also want to add a catch-all instance:
</p>
<pre class="wiki">instance MonadControlIO m ⇒ RegionControlIO m where
newtype RegionStIO m α = StIOG (StIO m α)
unsafeLiftControlIO f = liftControlIO $ \runInIO → f $ liftM StIOG ∘ runInIO
unsafeRestore (StIOG st) = restore st
</pre><p>
However this is not allowed because type families may not overlap:
</p>
<pre class="wiki">Conflicting family instance declarations:
newtype RegionStIO (RegionT s pr) α
newtype RegionStIO m α
</pre><p>
This is currently blocking me to use the new design of <tt>monad-control</tt> in my <tt>regions</tt> library.
</p>
TicketsimonpjWed, 09 Nov 2011 19:09:51 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:12
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:12
<p>
The trouble is that if both these instances were allowed, one could readily construct (in FC) a coercion making STIOG equal to STIOR. And that's unsound.
</p>
<p>
However I have been working with Dimitrios on an idea that would allow overlapping type function definitions, provided they were all declared together. So: would it be enough to allow overlapping type family instances, but <em>only if the overlapping ones were declared together</em> (or at least in the same module)?
</p>
<p>
Simon
</p>
TicketpumpkinWed, 09 Nov 2011 19:42:17 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:13
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:13
<ul>
<li><strong>cc</strong>
<em>pumpkingod@…</em> added
</li>
</ul>
<p>
It seems like now that we have lifted types into kinds, we can already define effectively closed type families (with a domain over a lifted type), which should be able to allow GHC to reason locally about overlap and completeness. Could that be used to help things along here?
</p>
TicketbasvandijkWed, 09 Nov 2011 20:26:28 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:14
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:14
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4259#comment:12" title="Comment 12">simonpj</a>:
</p>
<blockquote class="citation">
<p>
would it be enough to allow overlapping type family instances, but <em>only if the overlapping ones were declared together</em> (or at least in the same module)?
</p>
</blockquote>
<p>
Yes that would work here since both <tt>newtype RegionStIO (RegionT s pr) α</tt> and <tt>newtype RegionStIO m α</tt> are defined in the same module.
</p>
TicketnathanhowellSat, 21 Jan 2012 03:19:15 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:15
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:15
<ul>
<li><strong>cc</strong>
<em>nathanhowell@…</em> added
</li>
</ul>
TicketiglooThu, 09 Feb 2012 14:53:57 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:16
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:16
<ul>
<li><strong>milestone</strong>
changed from <em>7.4.1</em> to <em>7.6.1</em>
</li>
</ul>
TicketchoenerzsTue, 28 Feb 2012 15:18:46 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:17
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:17
<ul>
<li><strong>cc</strong>
<em>choener@…</em> added
</li>
</ul>
TicketduaircThu, 15 Mar 2012 16:59:49 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:18
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:18
<ul>
<li><strong>cc</strong>
<em>shane@…</em> added
</li>
</ul>
TicketduaircThu, 15 Mar 2012 17:24:54 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:19
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:19
<p>
I'd just like to point out that the following works (using functional dependencies):
</p>
<pre class="wiki">{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
class (Monad (Inner m), Monad m) => MonadLayer m where
type Inner m :: * -> *
lift :: Inner m a -> m a
class (Monad b, Monad m) => MonadBase b m | m -> b where
liftBase :: b a -> m a
instance MonadBase IO IO where
liftBase = id
instance (MonadLayer m, MonadBase b (Inner m)) => MonadBase b m where
liftBase = lift . liftBase
</pre><p>
While the following (using type families) does not:
</p>
<pre class="wiki">{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
class (Monad (Inner m), Monad m) => MonadLayer m where
type Inner m :: * -> *
lift :: Inner m a -> m a
class (Monad (Base m), Monad m) => MonadBase m where
type Base m :: * -> *
liftBase :: Base m a -> m a
instance MonadBase IO where
type Base IO = IO
liftBase = id
instance (MonadLayer m, MonadBase (Inner m)) => MonadBase m where
type Base m = Base (Inner m)
liftBase = lift . liftBase
</pre><p>
The example using functional dependencies will work even if the instances are defined in different modules.
</p>
TicketgoldfireTue, 10 Jul 2012 17:04:57 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:20
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:20
<ul>
<li><strong>cc</strong>
<em>eir@…</em> added
</li>
</ul>
TicketgoldfireTue, 21 Aug 2012 02:22:19 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:21
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:21
<p>
I (<a class="ext-link" href="http://www.cis.upenn.edu/~eir"><span class="icon"></span>Richard</a>) am working on adding overlapping type family instances and have documented my work on the <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/NewAxioms">NewAxioms</a> page. That work is somewhat orthogonal to the discussion here, but it touches on some of these issues. Of perhaps more direct interest is <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap">NewAxioms/CoincidentOverlap</a>, which directly continues the discussion started here. Any comments and/or feedback welcome.
</p>
TicketiglooWed, 12 Sep 2012 11:11:59 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:22
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:22
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.1</em> to <em>7.6.2</em>
</li>
</ul>
TicketgoldfireSun, 23 Dec 2012 05:15:35 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:23
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:23
<p>
The implementation of ordered type family instances is complete, and pushed to HEAD. A brief description of how it all works can be found <a class="ext-link" href="http://typesandkinds.wordpress.com/2012/12/22/ordered-overlapping-type-family-instances/"><span class="icon"></span>here</a>. In the process of writing this extension to type families, a lot of the issues discussed in this bug report came up, unfortunately without much resolution.
</p>
<p>
Because getting the overlap discussed here working with ordered overlap is delicate (we weren't quite sure how to do it and retain type soundness), ordered overlap and confluent overlap do not currently mix. Specifically, any instance declared with the <tt>type instance where</tt> syntax may not have confluent overlap with any other instance. It's conceivable that there is a way to make it all work together, but it's nontrivial, and without a compelling reason to do it, the feature may not be worth the implementation complexity.
</p>
<p>
It has also become clear that the ideas leading to this thread have a more general setting than just allowing for relaxed overlap restrictions. For example, given a type family for <tt>And</tt>, we may want GHC to be able to simplify <tt>And x y ~ True</tt> to <tt>(x ~ True, y ~ True)</tt>... but this is certainly not straightforward type family simplification. I'm still not quite sure what the solution is, but my thought is that simply relaxed restrictions on overlap will be 1) hard to do right and 2) not quite enough power anyway.
</p>
TicketliyangThu, 10 Jan 2013 09:14:23 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:24
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:24
<ul>
<li><strong>cc</strong>
<em>hackage.haskell.org@…</em> added
</li>
</ul>
<p>
Is milestone of 7.6.2 still correct, or is this only going into 7.8?
</p>
TicketiglooThu, 10 Jan 2013 16:44:28 GMTmilestone changed; difficulty set
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:25
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:25
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
changed from <em>7.6.2</em> to <em>7.8.1</em>
</li>
</ul>
<p>
We won't be making language changes within the 7.6 branch, so this will not happen before 7.8.
</p>
TicketcarterThu, 10 Jan 2013 21:03:31 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:26
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:26
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4259#comment:23" title="Comment 23">goldfire</a>:
</p>
<blockquote class="citation">
<p>
It has also become clear that the ideas leading to this thread have a more general setting than just allowing for relaxed overlap restrictions. For example, given a type family for <tt>And</tt>, we may want GHC to be able to simplify <tt>And x y ~ True</tt> to <tt>(x ~ True, y ~ True)</tt>... but this is certainly not straightforward type family simplification. I'm still not quite sure what the solution is, but my thought is that simply relaxed restrictions on overlap will be 1) hard to do right and 2) not quite enough power anyway.
</p>
</blockquote>
<p>
being able to "prove" (And x y) ~ True ---> (x~ True,y~True), and other things like it, that seems like it'd be a generalization of whats needed for Injective type families, right?
</p>
TicketgoldfireFri, 11 Jan 2013 02:57:13 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:27
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:27
<p>
Yes. The desire for injective type families (<a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/6018" title="feature request: Injective type families (new)">#6018</a>) and this report seem something like treating symptoms instead of the disease. (Don't take that simile too far -- I'm not suggesting GHC's current treatment is somehow diseased, just not as powerful as some want.) What we all seem to want (even if we don't know it) is the ability to define an arbitrary rewrite system over types and for GHC to somehow, magically check that our rewrite system is consistent and then to apply it. I'm pretty sure that goal is impossible. But, we can certainly make inroads in that direction. Relaxing restrictions on instance overlap as described here is one way, and injective type families is another.
</p>
<p>
My current thought on all of this is that we should consider some unified approach with a unified goal, instead of attacking this problem piecemeal. This unified approach may end up devolving into solving these two problems separately, but there should be an articulated reason why these two problems (this ticket and injectivity) are the two problems to solve.
</p>
TicketcarterFri, 11 Jan 2013 03:32:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:28
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:28
<p>
well said,
I have some thoughts on this. or at least my naive interpretation of a possible unifying point in the design space.
</p>
<p>
I'll add a note on it to this ticket once i've thought about it a bit more
</p>
TicketmorabbinThu, 04 Apr 2013 17:06:11 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:29
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:29
<ul>
<li><strong>cc</strong>
<em>andy.adamsmoran@…</em> added
</li>
</ul>
TicketgoldfireWed, 09 Oct 2013 02:19:07 GMTrelated set
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:30
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:30
<ul>
<li><strong>related</strong>
set to <em>#8423</em>
</li>
</ul>
<p>
See also <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8423" title="feature request: contraint solver doesn't reduce reducible closed type family ... (new)">#8423</a> to see an example of this issue in action in the context of closed type families.
</p>
TicketthoughtpoliceMon, 28 Apr 2014 12:41:18 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:31
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:31
<ul>
<li><strong>milestone</strong>
changed from <em>7.8.3</em> to <em>7.10.1</em>
</li>
</ul>
<p>
Moving to 7.10.1.
</p>
TicketjstolarekFri, 04 Jul 2014 09:32:20 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:32
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:32
<ul>
<li><strong>cc</strong>
<em>jan.stolarek@…</em> added
</li>
</ul>
TicketthoughtpoliceTue, 23 Dec 2014 13:34:10 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:33
http://ghc.haskell.org/trac/ghc/ticket/4259#comment:33
<ul>
<li><strong>milestone</strong>
changed from <em>7.10.1</em> to <em>7.12.1</em>
</li>
</ul>
<p>
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
</p>
Ticket