#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 chak):
Replying to [comment:2 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.)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:3>
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
