Opened 4 years ago

Last modified 6 months ago

#4259 new feature request

Relax restrictions on type family instance overlap

Reported by: lilac Owned by:
Priority: normal Milestone: 7.8.3
Component: Compiler (Type checker) Version: 6.12.1
Keywords: Cc: dimitris@…, v.dijk.bas@…, pumpkingod@…, nathanhowell@…, choener@…, shane@…, eir@…, hackage.haskell.org@…, andy.adamsmoran@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets: #8423

Description

The following reduced fragment of some real code is rejected, but could be accepted, by GHC:

{-# 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

GHC says:

    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

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.

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.

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.

Change History (30)

comment:1 Changed 4 years ago by simonpj

  • Blocked By 4232 added
  • Summary changed from Type family instance conflict checks could be smarter to Add overlapping instances for type families

If I'm getting this right, overlap is OK if, but only if, 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 (F [Int]) to Bool in one place, and to Char in another, and that's unsound. This is to do with soundness, not termination.

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.

comment:2 follow-up: Changed 4 years ago by lilac

  • Summary changed from Add overlapping instances for type families to Relax restrictions on type family instance overlap

I don't think that's an accurate summary. Section 7.7.2.2.2 of the user's guide says:

"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."

And indeed that is the case. The following code is accepted by GHC 6.12 today:

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

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.

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.

[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.]

comment:3 in reply to: ↑ 2 ; follow-up: Changed 4 years ago by chak

Replying to lilac:

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.

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.)

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.)

comment:4 Changed 4 years ago by simonpj

  • Cc dimitris@… added

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 LessEq are confluent, even though more than one may apply. I wonder whether this is an unusual example, or whether there are many like it?

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

type family F a
type instance F [a] = Bool
type instance F [Int] = Char

Now, the term F [Char] is unambiguously equal to Bool. But F [b] can't reduce, because we don't know what b will be instantiated to.

On reflection though, I was too hasty in making this suggestion yesterday. It might be fine for a source language, but I'm not sure how to express it in System FC, the intermediate language. If we have the above two rules as axioms we could just compose them in sequence to get Bool ~ Char which is obvious nonsense. The only decent approach I can see is for the first rule to take a proof that a is not Int, and that seems pretty complicated.

So I'm not sure of the best way to proceed here.

Simon

comment:5 Changed 4 years ago by chak

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.

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).

comment:6 in reply to: ↑ 3 Changed 4 years ago by lilac

Replying to chak:

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.

That is already the case for entities other than type family instances. For instance, in this code:

class Foo a where f :: a -> a
instance Foo Int where f = id
type family Bar a :: *
g a = f (a :: Bar Int)

If "type instance Bar Int = Int" is also visible, this code compiles. Otherwise, it does not.

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.

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).

(More over using different rules depending on whether UndecidableInstances are allowed is confusing, too.)

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:

"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."

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.

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:

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.

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 here 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.

comment:7 Changed 4 years ago by igloo

  • Blocked By 4232 removed

comment:8 Changed 4 years ago by igloo

  • Milestone set to 7.0.1

comment:9 Changed 3 years ago by simonpj

  • Milestone changed from 7.0.1 to 7.2.1

We clearly aren't going to do this in 7.0, so re-milestoning.

comment:10 Changed 2 years ago by basvandijk

  • Cc v.dijk.bas@… added

comment:11 Changed 2 years ago by basvandijk

I would like to give another use-case for overlapping type family instances:

As explained in ticket #5595 I'm giving monad-control a new design.

My regions package uses monad-control 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:

For safety-reasons I don't want to make RegionT an instance of MonadControlIO. However I do need the ability to lift control operators like bracket or alloca into regions.

So what I did is, I created a class which is isomorphic to MonadControlIO called RegionControlIO. Just like MonadControlIO has the method liftControlIO, this class has the method unsafeLiftControlIO. This method however is only exported from the Unsafe module. So users are warned when using it. (I plan to use SafeHaskell to formalize this)

I made RegionT an instance of RegionControlIO:

instance RegionControlIO pr ⇒ RegionControlIO (RegionT s pr) where
    unsafeLiftControlIO f = ...

Besides that I added a catch-all instance:

{-# LANGUAGE OverlappingInstances #-}

instance MonadControlIO m ⇒ RegionControlIO m where
    unsafeLiftControlIO = liftControlIO

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: RegionT s1 (RegionT s2 (RegionT s3 (StateT Int (WriterT String IO))))

Now back to the problem. As said, I'm adapting regions to use the new design of monad-control. The RegionControlIO type class now looks like this:

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 β)

regions are again made an instance of this type class:

instance RegionControlIO pr ⇒ RegionControlIO (RegionT s pr) where
    newtype RegionStIO (RegionT s pr) α = StIOR (RegionStIO pr ... α))

    unsafeLiftControlIO f = ...

    unsafeRestore (StIOR stIO) = ...

As before, I also want to add a catch-all instance:

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 

However this is not allowed because type families may not overlap:

Conflicting family instance declarations:
  newtype RegionStIO (RegionT s pr) α
  newtype RegionStIO m α

This is currently blocking me to use the new design of monad-control in my regions library.

comment:12 follow-up: Changed 2 years ago by simonpj

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.

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 only if the overlapping ones were declared together (or at least in the same module)?

Simon

comment:13 Changed 2 years ago by pumpkin

  • Cc pumpkingod@… added

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?

comment:14 in reply to: ↑ 12 Changed 2 years ago by basvandijk

Replying to simonpj:

would it be enough to allow overlapping type family instances, but only if the overlapping ones were declared together (or at least in the same module)?

Yes that would work here since both newtype RegionStIO (RegionT s pr) α and newtype RegionStIO m α are defined in the same module.

comment:15 Changed 2 years ago by nathanhowell

  • Cc nathanhowell@… added

comment:16 Changed 2 years ago by igloo

  • Milestone changed from 7.4.1 to 7.6.1

comment:17 Changed 2 years ago by choenerzs

  • Cc choener@… added

comment:18 Changed 2 years ago by duairc

  • Cc shane@… added

comment:19 Changed 2 years ago by duairc

I'd just like to point out that the following works (using functional dependencies):

{-# 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

While the following (using type families) does not:

{-# 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

The example using functional dependencies will work even if the instances are defined in different modules.

comment:20 Changed 22 months ago by goldfire

  • Cc eir@… added

comment:21 Changed 20 months ago by goldfire

I (Richard) am working on adding overlapping type family instances and have documented my work on the NewAxioms page. That work is somewhat orthogonal to the discussion here, but it touches on some of these issues. Of perhaps more direct interest is NewAxioms/CoincidentOverlap, which directly continues the discussion started here. Any comments and/or feedback welcome.

comment:22 Changed 19 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:23 follow-up: Changed 16 months ago by goldfire

The implementation of ordered type family instances is complete, and pushed to HEAD. A brief description of how it all works can be found here. 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.

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 type instance where 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.

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 And, we may want GHC to be able to simplify And x y ~ True to (x ~ True, y ~ True)... 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.

comment:24 Changed 15 months ago by liyang

  • Cc hackage.haskell.org@… added

Is milestone of 7.6.2 still correct, or is this only going into 7.8?

comment:25 Changed 15 months ago by igloo

  • Difficulty set to Unknown
  • Milestone changed from 7.6.2 to 7.8.1

We won't be making language changes within the 7.6 branch, so this will not happen before 7.8.

comment:26 in reply to: ↑ 23 Changed 15 months ago by carter

Replying to goldfire:

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 And, we may want GHC to be able to simplify And x y ~ True to (x ~ True, y ~ True)... 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.

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?

comment:27 Changed 15 months ago by goldfire

Yes. The desire for injective type families (#6018) 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.

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.

comment:28 Changed 15 months ago by carter

well said,
I have some thoughts on this. or at least my naive interpretation of a possible unifying point in the design space.

I'll add a note on it to this ticket once i've thought about it a bit more

comment:29 Changed 13 months ago by morabbin

  • Cc andy.adamsmoran@… added

comment:30 Changed 6 months ago by goldfire

See also #8423 to see an example of this issue in action in the context of closed type families.

Note: See TracTickets for help on using tickets.