Re: [GHC] #14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary

1 Aug 2017

      #14045: Data family instances must list all patterns of family, despite
documentation's claims to the contrary
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:  indexed-
  valid program                      |  types/should_compile/T14045,
                                     |  indexed-types/should_fail/T14045a
      Blocked By:                    |             Blocking:
 Related Tickets:  #12369            |  Differential Rev(s):  Phab:D3804
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Yes, you're right.  What I should have said is this.

 There is no reason to allow data instances to be written under-saturated.
 That is, we could insist on
 {{{
 data instance Sing (a :: Bool) where ...
 }}}
 But, as an additional feature, we allow you to drop any trailing patterns
 that are simply type variables (if not mentioned earlier).  Thus
 {{{
 data instance T Int [a] (c::*) (d::Bool) (e::*)  where ...
 }}}
 can also be written equivalently
 {{{
 data instance T Int [a] :: * -> Bool -> * -> * where ...
 }}}
 Is that right? If so, let's update the user manual to say so.

 Alas, we have a bug, I think. Consider
 {{{
 data family T a b :: Type

 newtype instance T Int :: Type -> Type where
   MkT :: IO a -> T Int a
   deriving( Monad, Applicative, Functor )
 }}}
 Oddly, this fails with
 {{{
 Foo2.hs:38:13: error:
     • Can't make a derived instance of ‘Monad (T Int)’
         (even with cunning GeneralizedNewtypeDeriving):
         cannot eta-reduce the representation type enough
 }}}
 Whereas this succeeds
 {{{
 newtype instance T Int a :: Type where
   MkT :: IO a -> T Int a
   deriving( Monad, Applicative, Functor )
 }}}
 so the two aren't (yet) quite equivalent.  Do you agree this is a bug?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:13
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler