#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
----------------------------------------+-----------------------------------
Changes (by simonpj):
* cc: dimit...@… (added)
Comment:
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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
