GitLab

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.

Trac metadata

Trac field	Value
Version	6.12.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture