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

21 Jan 2016


      #11449: Treat '_' consistently in type declarations
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

@@ -11,2 +11,2 @@
- class C [_] where         -- Not allowed
-   type T [_] = Int   -- Not allowed
+ instance C [_] where         -- Not allowed
+   type T [_] = Int           -- Not allowed

New description:

 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
 instance 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#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

    