#12680: Permit type equality instances in signatures -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): For the most part, I think we want an "abstract type synonym" to behave like an open type family with no (known) equations. So wherever we see `type S :: * -> *`, it should be as if we see `type family S :: * -> *`. We must relax the signature matching rules to allow a type family to be implemented using a type synonym. I think it's sound to behave this way, because `type S = Foo` can always be interpreted as `type instance S = Foo`. There is two things to watch out for, however. First, consider the following program: {{{ signature H where type S f :: Int module M where type S = Int f :: S }}} We would like M to match H, but if S is an open type family, the match will fail: S is not definitionally equal to Int, and matching is done strictly with definitional equality. I don't think we should change this for now: with more complex matching we will have to generate coercions to keep Core well-typed. So, instead, we just want to replace the open type family tycon with a type synonym tycon (in the same way an abstract algebraic data type gets replaced with the full data type). This is only sound if, when a module typechecks, it continues to typecheck if more definitional equalities hold. This is actually not true; `instance Show T` and `instance Show S` will overlap if T is definitionally equal to S! But we knew that already: we can implement an abstract algebraic data type with a reexport (which will cause more definitional equalities to hold), and fortunately, Scott showed that this *is* sound in Haskell without instances, so it will do something vaguely reasonable. So, that was a really long way of justifying why we can't just search replace `type S` with `type family S` and `type S = Int` with `type family S = Int`. Second, consider the following program: {{{ signature H where type F a instance Show a => Show (F a) }}} We'd really like this to work. But if F is implemented with type family (or a type synonym to a type family), this instance is illegal and can't be implemented. So what we want to be able to say is that `type F a` can be implemented with a type synonym, but *only* a type synonym with no type families in it. There doesn't seem to be a good way to make a claim like this in the language. But given that ``type family F a`` is still a fair way to specify a type family, perhaps the correct thing to do in this case is to just say that an abstract type can only be implemented by a type synonym with no type families, and check that upon matching. So the abstract type synonym really is a beast of its own: it is like an open type synonym family (in that it is not reducible, but could become reducible in the future), BUT it should still be accepted in instances, because once we *do* know how it's reducible, there will be no more type families left. By the way, this discussion informed me of another problem: {{{ {-# LANGUAGE TypeFamilies #-} unit bar where signature H1 where data T signature H2 where data T module M where import qualified H1 import qualified H2 f :: (H1.T ~ H2.T) => a -> b f x = x }}} This typechecks! Today, the solver concludes that ``H1.T ~ H2.T`` is insoluble and accepts the rest of the function. But if H1 and H2 are instantiated in the same way, this equality could hold! So, for abstract data types from signatures (not boots) we better treat this differently. So let us summarize: * Abstract data types `data T a` can be implemented by a data type or newtype declaration. We can assume that they are injective on all type parameters and can be used in instances. * Abstract type synonyms `type T a` can be implemented by a type synonym (with no type families), data type or newtype declaration. They can be used in instances. Arguably it should be possible to specify their injectivity (in the absence of type families, they are either injective or not used at all). I guess it should also be possible to specify their role. * Open type families `type family T a` can be implemented by a type family, type synonym, data type or newtype. Injectivity can be specified in the usual way. Roles are irrelevant. Abstract type synonyms should probably be implemented as abstract data types that are not assumed to be injective; furthermore, both abstract data types and abstract type synonyms need to account for the fact that they might eventually become definitionally equal to something else. I am not so sure how this should happen; if we model off of open type families, the correct thing to do is flatten it with a fresh skolem variable, but this will thwart instance declarations, which is undesirable. So we will need to do something else. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12680#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler