#4259: Type family instance conflict checks could be smarter
---------------------------------+------------------------------------------
Reporter: lilac | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 6.12.1 | Keywords:
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4259>
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
