[GHC] #12680: Permit type equality instances in signatures

[GHC]

#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