#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):
I don't think that's an accurate summary. Section 7.7.2.2.2 of the
[http://www.haskell.org/ghc/docs/6.12.1/html/users_guide/type-
families.html 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.]
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259#comment:2>
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
