#4259: Relax restrictions on type family instance overlap
----------------------------------------+-----------------------------------
Reporter: lilac | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.12.1
Keywords: | Testcase:
Blockedby: 4232 | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by lilac):
Replying to [comment:3 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
[http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
