[GHC] #11449: Treat '_' consistently in type declarations

18 Jan 2016

      #11449: Treat '_' consistently in type declarations
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC doesn't treat `_` consistently in type declarations
 {{{
 -- Example A
 data T _ = MkT            -- Not allowed

 -- Example B
 class C a where
   type T a

 -- Example C
 class C [_] where         -- Not allowed
   type T [_] = Int   -- Not allowed

 -- Example D
 data family D a
 data instance D [_] = MkD   -- Allowed

 -- Example E
 type family F a
 type instance F [_] = Int   -- Allowed
 }}}
 This seems inconsistent and annoying (see
 [https://mail.haskell.org/pipermail/glasgow-haskell-
 users/2016-January/026114.html email thread]).

 Really, we should consistently treat `_` in a binding position simply as
 ''a binder that binds nothing'', just like at the term level.

 But in Haskell 98 `_` is a reserved identifier, so these programs are
 illegal.  We use `PartialTypeSignatures` to allow `_` in occurrence
 positions in types.  Should the same flag enable `_` in binding positions?
 It would seem a little odd to require `PartialTypeSignatures` for (A) and
 (C).

 Any suggestions?

 A couple of wrinkles.  First, since `_` binds nothing, it certainly
 doesn't bind occurrences of `_`.  Thus for example, with
 `PartialTypeSignatures`
 {{{
 instance C [_] where
   op = .... (let f :: _ -> _
                 f = e
              in ...) ...
 }}}
 The occurrences of `_` in `op`'s RHS are ''not'' bound by the `_` in the
 `instance` header.  (The would be if all three were `a`, say.)  Rather the
 occurrences of `_` are holes in the type signature and should be
 separately reported as such.

 Second, the implementation would be tricky in one spot:
 {{{
 class C a where
   type T a

 instance C (Either _ _) where
   type T (Either _ _) = ...
 }}}
 We must check that the type family instance is at the same type as the
 class.  Do we want to insist that it looks ''exactly'' the same, or would
 you be allowed to say this?
 {{{
 instance C (Either _ _) where
   type T (Either a b) = a -> b
 }}}
 My instinct is to say "exactly the same" for now anyway.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler