Opened 2 years ago

Closed 2 years ago

#14045 closed bug (fixed)

Data family instances must list all patterns of family, despite documentation's claims to the contrary

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.3
Keywords: TypeFamilies Cc: Iceland_jack, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_compile/T14045, indexed-types/should_fail/T14045a, deriving/should_compile/T14045b
Blocked By: Blocking:
Related Tickets: #12369 Differential Rev(s): Phab:D3804
Wiki Page:

Description

(Originally spun off from #12369.)

The documentation for data families currently claims:

- Data families have been generalised a bit: a data family declaration can now
  end with a kind variable ``k`` instead of ``Type``. Additionally, data/newtype
  instance no longer need to list all the patterns of the family if they don't
  wish to; this is quite like how regular datatypes with a kind signature can omit
  some type variables.

Moreover, the commit which added this (4239238306e911803bf61fdda3ad356fd0b42e05) cites this particular example:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

However, in practice, this does not typecheck on GHC HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

data family Sing (a :: k)
data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:8:1: error:
    • Number of parameters must match family declaration; expected 0
    • In the data instance declaration for ‘Sing’
  |
8 | data instance Sing :: Bool -> Type where
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Change History (18)

comment:1 Changed 2 years ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 2 years ago by RyanGlScott

Similarly, associated data family instances of this form are also rejected:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

class C (a :: k) where
  data Sing (a :: k)

instance C (z :: Bool) where
  data Sing :: Bool -> Type where
    SFalse :: Sing False
    STrue  :: Sing True
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:12:3: error:
    • Number of parameters must match family declaration; expected 0
    • In the data instance declaration for ‘Sing’
      In the instance declaration for ‘C (z :: Bool)’
   |
12 |   data Sing :: Bool -> Type where
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

I'm not sure if such a thing would be permissible, since GHC imposes some additional restrictions on the type patterns of associated family instances. If it's not permissible, we should give a better error message here.

comment:3 Changed 2 years ago by simonpj

Cc: goldfire added

To me the k argument to Sing looks like an invisible (implicit) one. So you should need visible kind application to use it in an invocation, something like

instance C (z :: Bool) where
  data Sing :: Bool -> Type where
    SFalse :: Sing @False
    STrue  :: Sing @True

Let's see what Richard says.

comment:4 Changed 2 years ago by goldfire

Differential Rev(s): Phab:D3804

Well, that's embarrassing. Easy enough to fix, but annoying to get good error messages in the mismatched associated type case (comment:2, which I think should be rejected).

I'm afraid I think comment:3 is in error -- I don't understand what you're getting at.

comment:5 Changed 2 years ago by Richard Eisenberg <rae@…>

In d1ef223c/ghc:

Fix #14045 by omitting an unnecessary check

Previously, we checked the number of patterns in a data instances
for all data families whose kind did not end in a kind variable.
But, of course, undersaturating instances can happen even without
the kind ending in a kind variable. So I've omitted the arity check.
Data families aren't as particular about their arity as type families
are (because data families can be undersaturated). Still, this change
degrades error messages when instances don't have the right arity;
now, instead of reporting a simple mismatch in the number of patterns,
GHC reports kind errors. The new errors are fully accurate, but perhaps
not as easy to work with. Still, with the new flexibility of allowing
data family instances with varying numbers of patterns, I don't see
a better way.

This commit also improves source fidelity in some error messages,
requiring more changes than really are necessary. But without these
changes, error messages around mismatched associated instance heads
were poor.

test cases: indexed-types/should_compile/T14045,
            indexed-types/should_fail/T14045a

comment:6 Changed 2 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T14045, indexed-types/should_fail/T14045a

All set now.

comment:7 Changed 2 years ago by simonpj

I don't see in the patch where an arity check is omitted.

And I'd love a Note somewhere giving examples of "Data families aren't as particular about their arity as type families are (because data families can be undersaturated)", at some relevant point in the type checker. The point is, I guess, that

data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True

and

data instance Sing (a :: Bool) :: Type where
  SFalse :: Sing False
  STrue  :: Sing True

are similar, but not quite the same. Moreover, different instances can make different choices. Moreover you can't to that for type families. We should call that out somewhere, and explain why it's different (data families can be decomposed, type families can't).

I'll re-open for such a note, if that's ok.

Last edited 2 years ago by simonpj (previous) (diff)

comment:8 Changed 2 years ago by simonpj

Resolution: fixed
Status: closednew

comment:9 Changed 2 years ago by Richard Eisenberg <rae@…>

In c6d4219a/ghc:

Clarify comment about data family arities

as requested in #14045.

[skip ci] comments only

comment:10 Changed 2 years ago by goldfire

Does that do it? It's all in Note [Arity of data families] in FamInstEnv.

Also, the skipped arity check in the previous patch is in tc_fam_ty_pats in TcTyClsDecls.

comment:11 Changed 2 years ago by simonpj

Ah I missed the reference to Note [Arity of data families]. Thanks. But

     This instance is very nearly equivalent to
        data instance Sing (a :: Bool) where ...
     but without the last pattern, we have an under-saturated data
     family instance.  On its own, this example is not compelling

Can you say more precisely what /is/ the difference? Is it only the newtype-eta thing? Or is there anything else?

comment:12 Changed 2 years ago by goldfire

There isn't a difference.

data instance Sing (a :: Bool) where ...

and

data instance Sing :: Bool -> Type where ...

compile to precisely the same internal representation. It's the same because the first one gets eta-reduced to look like the second. That's why the note says

This instance is equivalent to `data instance Sing (a :: Bool)`

I'm not sure where you get "very nearly equivalent" above.

comment:13 Changed 2 years ago 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?

comment:14 Changed 2 years ago by RyanGlScott

Do you agree this is a bug?

I certainly do. In the bowels of TcDeriv, we check that newTyConEtadRhs (the eta-reduced representation type) can accommodate the number of arguments from the instance we're deriving. But after doing some pprTrace scavenging, I discovered that the newTyConEtadRhs for newtype instance T Int :: Type -> Type is

([a_a1vc], IO a_a1vc)

Whereas for newtype instance T Int a :: Type, it's:

([], IO)

Something fishy is going on. The result of newTyConEtadRhs is ultimately being created in mkNewTyConRhs, which computes the eta-reduced type variables by checking one-by-one if a tycon tyvar matches the tyvar in the representation type in the corresponding position (see eta_reduce).

My guess is that this a_a1vc tyvar from the representation type doesn't match the corresponding tyvar from newtype instance T Int :: Type -> Type (what would the corresponding tyvar be, anyway?)

comment:15 Changed 2 years ago by simonpj

I found it. Patch coming.

comment:16 Changed 2 years ago by simonpj

I ran out of time, got stuck upgrading to GHC 8 which is now required...

Here is the patch: Ryan, would you like to validate and commit?

simonpj@cam-05-unx:~/code/HEAD$ git show 143f08a3
commit 143f08a32b80f7f80d77b518ce207a1051368b9e
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Aug 2 15:57:21 2017 +0100

    Get the roles right for newtype instances
    
    This was a simple slip, that gave rise to the bug reported in
    comment:13 of Trac #14045.  We were supplying roles to mkAlgTyCon
    that didn't match the tyvars.

diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index fe513f4..58d4506 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -695,7 +695,7 @@ tcDataFamInstDecl mb_clsinfo
                       -- the end of Note [Data type families] in TyCon
                     rep_tc   = mkAlgTyCon rep_tc_name
                                           ty_binders liftedTypeKind
-                                          (map (const Nominal) full_tvs)
+                                          (map (const Nominal) ty_binders)
                                           (fmap unLoc cType) stupid_theta
                                           tc_rhs parent
                                           gadt_syntax
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index b81192f..dcc134c 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1315,8 +1315,12 @@ mkLamType v ty
 
 mkLamTypes vs ty = foldr mkLamType ty vs
 
--- | Given a list of type-level vars and a result type, makes TyBinders, preferring
--- anonymous binders if the variable is, in fact, not dependent.
+-- | Given a list of type-level vars and a result kind,
+-- makes TyBinders, preferring anonymous binders
+-- if the variable is, in fact, not dependent.
+-- e.g.    mkTyConBindersPreferAnon [(k:*),(b:k),(c:k)] (k->k)
+-- We want (k:*) Named, (a;k) Anon, (c:k) Anon
+--
 -- All binders are /visible/.
 mkTyConBindersPreferAnon :: [TyVar] -> Type -> [TyConBinder]
 mkTyConBindersPreferAnon vars inner_ty = fst (go vars)
diff --git a/testsuite/tests/deriving/should_compile/T14045.hs b/testsuite/tests/deriving/should_compile/T14045.hs
new file mode 100644
index 0000000..d721a3d
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14045.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, KindSignatures, GADTs, GeneralizedNewtypeDeriving #-}
+
+module T14045 where
+
+import Data.Kind ( Type )
+
+data family T a b :: Type
+
+-- newtype instance T Int d = MkT (IO d)
+
+newtype instance T Int :: Type -> Type where
+   MkT :: IO d -> T Int d
+  deriving( Monad, Applicative, Functor )
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 0025d25..10e2e60 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -94,3 +94,4 @@ test('drv-phantom', [normalise_errmsg_fun(just_the_deriving)],compile, ['-ddump-
 test('T13813', normal, compile, [''])
 test('T13919', normal, compile, [''])
 test('T13998', normal, compile, [''])
+test('T14045', normal, compile, [''])

Thanks!

comment:17 Changed 2 years ago by Ryan Scott <ryan.gl.scott@…>

In d74983ef/ghc:

Get the roles right for newtype instances

This was a simple slip, that gave rise to the bug reported in
comment:13 of Trac #14045.  We were supplying roles to mkAlgTyCon
that didn't match the tyvars.

comment:18 Changed 2 years ago by RyanGlScott

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T14045, indexed-types/should_fail/T14045aindexed-types/should_compile/T14045, indexed-types/should_fail/T14045a, deriving/should_compile/T14045b

Done. Thanks, Simon!

Note: See TracTickets for help on using tickets.