Opened 2 years ago

Closed 2 years ago

#14131 closed bug (fixed)

Difference between newtype and newtype instance

Reported by: Iceland_jack Owned by: RyanGlScott
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.2.1
Keywords: TypeFamilies Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T14131
Blocked By: #13988 Blocking:
Related Tickets: #7938, #9574, #13985 Differential Rev(s): Phab:D3872, Phab:D3881
Wiki Page:

Description

This works

{-# Language RankNTypes, PolyKinds, GADTs #-}

newtype Nat :: (k -> *) -> (k -> *) -> * where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

but this

{-# Language RankNTypes, PolyKinds, GADTs, TypeFamilies #-}

data family Nat :: k -> k -> *

newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

fails on GHC 8.3.20170815, and requires a forall k. to work

$ ./ghc-stage2 -ignore-dot-ghci --interactive /tmp/kind.hs 
GHCi, version 8.3.20170815: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/kind.hs, interpreted )

/tmp/kind.hs:5:26: error: Not in scope: type variable ‘k’
  |
5 | newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  |                          ^

/tmp/kind.hs:5:38: error: Not in scope: type variable ‘k’
  |
5 | newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  |                                      ^
Failed, 0 modules loaded.

Related to #12369?

Change History (23)

comment:1 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added
Keywords: TypeFamilies added

comment:2 Changed 2 years ago by goldfire

No. Not really related to #12369. Perhaps related to #13985. Perhaps not.

comment:3 Changed 2 years ago by RyanGlScott

Note that this error does not occur if the kind variables are bound in an earlier type pattern. That is, this equivalent instance typechecks:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

data family Nat :: k -> k -> *

newtype instance Nat (f :: k -> *) :: (k -> *) -> * where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

comment:4 Changed 2 years ago by RyanGlScott

After tinkering around with this example some more, I realized that the problem isn't limited to just data family instances—this affects type families across the board. Namely, type families do not implicitly bind kind variables that users write in result signatures.

That is, this type synonym definition is legal:

{-# LANGUAGE DataKinds #-}                                                                         
{-# LANGUAGE PolyKinds #-}                                                                         
                                                                                                   
type F = (Nothing :: Maybe a)

But this type family instance is not legal:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

type family   F :: Maybe a
type instance F = (Nothing :: Maybe a)
GHCi, version 8.3.20170816: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:6:37: error: Not in scope: type variable ‘a’
  |
6 | type instance F = (Nothing :: Maybe a)
  |                                     ^

I don't see any reason why the latter definition should be rejected. One could object that all the type variables in a type family instance must be bound on the LHS type patterns. But really, the a is Maybe a is bound by the often-neglected RHS type pattern. This is made more evident by the fact that tweaking the code to avoid the explicit Maybe a kind ascription makes it typecheck:

type instance F = Nothing

However, if you inspect F with :info in GHCi with the -fprint-explicit-kinds flag enabled, then you discover that you end up achieving the same result in the end:

λ> :set -fprint-explicit-kinds 
λ> :i F
type family F a :: Maybe a      -- Defined at Bug.hs:5:1
type instance F a = 'Nothing a  -- Defined at Bug.hs:6:15

Here, it becomes evident that the kind variable a in Maybe a is being implicitly bound. But alas, GHC won't let you write it out explicitly.

This becomes even more infuriating when dealing with associated type instances. For example, I tried to write this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

class C k where
  type T :: k

instance C (Maybe a) where
  type T = (Nothing :: Maybe a)
GHCi, version 8.3.20170816: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:9:3: error:
    The RHS of an associated type declaration mentions ‘a’
      All such variables must be bound on the LHS
  |
9 |   type T = (Nothing :: Maybe a)
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Once again, GHC mistakenly assumes that a must be bound in a LHS type pattern. But the whole point of T is that the instance is determined by the RHS type pattern! So as a workaround, I must leave off the explicit kind signature.

comment:5 Changed 2 years ago by goldfire

Good sleuthing here. Do you think you can fix the bug? I don't think it would be too hard. My guess is that fixing this in concert with #13985 will work nicely.

comment:6 in reply to:  5 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3872
Status: newpatch

Replying to goldfire:

Do you think you can fix the bug?

You got it! See Phab:D8372, which also fixes #13985 and #13988.

comment:7 Changed 2 years ago by RyanGlScott

It's also worth noting that Phab:D3872 reverses a design decision made in #7938 and #9574 to only allow kind variables in the RHSes of associated type instances if they're explicitly bound by LHS type patterns. But I think this is the right thing to do, because otherwise you can't have things like:

class C k where
  data family Nat :: k -> k -> Type

instance C (k -> Type) where
  newtype Nat :: (k -> Type) -> (k -> Type) -> Type where
    Nat :: (forall xx. f xx -> g xx) -> Nat f g

And rejecting this feels like the wrong stance to take.

comment:8 Changed 2 years ago by simonpj

It's also worth noting that ​Phab:D3872 reverses a design decision made in #7938 and #9574 to only allow kind variables in the RHSes of associated type instances if they're explicitly bound by LHS type patterns.

I don't think it reverses it. We just didn't implement it properly. If we wrote out the kind arguments we'd see

class C k where
  data family Nat @k :: k -> k -> Type

instance C (k -> Type) where
  newtype Nat @(k -> Type) :: (k -> Type) -> (k -> Type) -> Type where
    Nat :: forall k (f::k->Type) (g::k->Type).
           (forall xx. f xx -> g xx) -> Nat @(k->Type) f g

So that k certainly is bound on the left, in the (invisible) kind pattern. (Side note: it's jolly confusing that, in this example, the kind argument is visible for the class but invisible for the associated type.)

But really, the a is Maybe a is bound by the often-neglected RHS type pattern.

I don't like this language. There is no "RHS type pattern". Rather, there are invisible kind patterns on the LHS.

And this matters! Consider

type family T (a :: Type) :: Type
type family F :: k

type instance T Int = Proxy (F :: k)

Now T does not have a kind parameter, and that k on the RHS of the type instance really is unbound. Writing out the kind arguments:

type instance T Int = Proxy @k (F @k)

which is manifestly wrong.

Bottom line: we can't distinguish the two cases in the renamer. We have to check this in the type checker. Nevertheless, the renamer must not prematurely reject the instance. So the renamer must (optimistically) bring the RHS type/kind variables into scope; the type checker may subsequently reject.

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

comment:9 Changed 2 years ago by simonpj

I'm not happy with Phab:D3872. Currently we have

type HsTyPats pass = HsImplicitBndrs pass [LHsType pass]

That sugggests that the implicit binders scope only over the patterns. But as we know, they don't. They scope over the RHS too. And indeed, as this ticket discusses, we may have variables that are implicitly bound in the RHS, but are not even mentioned on the LHS.

These HsTyPats are used in DataFamInstDecl and TyFamInstEqn (only). For the latter: Currently we have

type TyFamInstEqn  pass = TyFamEqn pass (HsTyPats pass)
type TyFamDefltEqn pass = TyFamEqn pass (LHsQTyVars pass)

data TyFamEqn pass pats
  = TyFamEqn
       { tfe_tycon  :: Located (IdP pass)
       , tfe_pats   :: pats
       , tfe_fixity :: LexicalFixity    -- ^ Fixity used in the declaration
       , tfe_rhs    :: LHsType pass }

where the implicit binders inside tfe_pats weirdly scopes over the tfe_rhs. Instead we can have

type TyFamInstEqn  pass = HsImplicitBndrs (TyFamEqn pass [HsType pass])
type TyFamDefltEqn pass = HsImplicitBndrs (TyFamEqn pass [LHsTyVarBndr pass])

I have not worked through the details, but it seems right to wrap the implicit binders around everything that they scopes over. I suspect that'll make the code easier too.

It's similar for DataFamInstDecl. Currently we have:

data DataFamInstDecl pass
  = DataFamInstDecl
       { dfid_tycon     :: Located (IdP pass)
       , dfid_pats      :: HsTyPats   pass
       , dfid_fixity    :: LexicalFixity
       , dfid_defn      :: HsDataDefn pass
       , dfid_fvs       :: PostRn pass NameSet }

Instead we could have

type DataFamInstDecl pass                  -- Implicit bndrs here
  = HsImplicitBndrs pass (DataFamInstEqn pass)

data DataFamInstEqn pass
  = DataFamInstEqn
       { dfid_tycon     :: Located (IdP pass)
       , dfid_pats      :: [LHsType pass]  -- No implicit bndrs
       , dfid_fixity    :: LexicalFixity
       , dfid_defn      :: HsDataDefn pass
       , dfid_fvs       :: PostRn pass NameSet }

Bubt that's still a bit strange, because the dfid_fvs should really be outside the HsImplicitBndrs. (And it is for TyFamEqn. So perhaps a better way would be to make DataFamInstDecl and TyFamInstDecl look a bit more like each other, thus

type DataFamInstDecl pass = FamInstDecl pass (HsDataDefn pass)
type TyFamINstDecl   pass = FamInstDecl pass (LHsType    pass)

data FamInstDecl pass rhs
  = FamInstDecl
       { fid_eqn  :: LFamInstEqn pass rhs
       , fid_fvs  :: PostRn pass NameSet }

type LFamInstEqn pass rhs = Located (FamInstEqn pass rhs)

type FamInstEqn pass rhs = HsImplicitBndrs (FamEqn pass [LHsType] rhs)

data FamEqn pass pats rhs
  = TyFamEqn
       { tfe_tycon  :: Located (IdP pass)
       , tfe_pats   :: pats
       , tfe_fixity :: LexicalFixity
       , tfe_rhs    :: rhs }

We still need the typechecker test for comment:8.

Finally: we need user-manual comments to explain what's accepted and what is rejected.

comment:10 in reply to:  9 Changed 2 years ago by RyanGlScott

Owner: set to RyanGlScott

The refactoring suggested in comment:9 sounds good to me. But perhaps I should first do this refactoring in a separate commit, since doing all of this datatype reshuffling and fixing the bugs in #14131 and #13985 simultaneously might be a touch too much.

Replying to simonpj:

We still need the typechecker test for comment:8.

Phab:D3872 has this in the form of the testsuite/tests/polykinds/T13985.hs test.

Finally: we need user-manual comments to explain what's accepted and what is rejected.

Phab:D3872 has this already. Done.

comment:11 Changed 2 years ago by simonpj

We still need the typechecker test for comment:8.

What I mean is: the renaner cannot reject the right set of programs (see comment:8). So the renamer must err on the side of acceptance, and leave the type checker to reject programs where variables appear on the RHS that are not bound on the left.

But perhaps I should first do this refactoring in a separate commit

Sounds good to me.

comment:12 in reply to:  11 Changed 2 years ago by RyanGlScott

Replying to simonpj:

What I mean is: the renaner cannot reject the right set of programs (see comment:8). So the renamer must err on the side of acceptance, and leave the type checker to reject programs where variables appear on the RHS that are not bound on the left.

Right, this is exactly what Phab:D3872 is doing at the moment. In particular, it changes TcTyClsDecls so that we check for free-floating kind variables (or, as you put it, variables that appear on the RHS that are not bound on the left) when typechecking family instances.

comment:13 Changed 2 years ago by simonpj

Really? reportFloatingKvs seems to report variables mentioned in typat_tvs, which doesn't look like the ones on the RHS. I wasn't expecting a test in tcFamTyPats, but rather in tcTyFamInstEqn.

DO you have a test like the example in comment:8?

comment:14 in reply to:  13 Changed 2 years ago by RyanGlScott

Replying to simonpj:

Really? reportFloatingKvs seems to report variables mentioned in typat_tvs, which doesn't look like the ones on the RHS. I wasn't expecting a test in tcFamTyPats, but rather in tcTyFamInstEqn.

Ah, I think I managed to confuse you by naming that variable typat_tvs. Those are the type variables that are used in type patterns (visible and invisible) or the RHS (these are collected during renaming, see rnFamInstDecl). We discover in tcFamTyPats which variables are actually bound by type patterns, so if there are any used variables that aren't bound, then they're free-floating (and summarily rejected).

I suppose I should rename typat_tvs to something like fam_used_tvs to avoid this confusion.

DO you have a test like the example in comment:8?

Yes, see testsuite/tests/polykinds/T13985.hs. In the particular case of type family instances, it tests this:

type instance T = Proxy (Nothing :: Maybe a)

Which is rejected for having a free-floating a.

comment:15 Changed 2 years ago by simonpj

Ah, I think I managed to confuse you

I am indeed terribly confused. I can now just about see what you are doing.

  • The hsib_vars wrapped around the HsTyPats includes (via the renamer) the variables mentioned in the RHS. You arrange that tc_fam_ty_pats returns them to its caller.
  • Now in tcFamTyPats you can take that set of variables, and subtract from it those bound on the LHS (gotten from the free vars of the typechecked pates). Result is the ones on the RHS but not LHS.

Ugh!

I bet that all this will look different, and much more perspicous, once we've done the refactoring in comment:9. As you suggest, let's do that first. Yell if you need any help

comment:16 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3872Phab:D3872, Phab:D3881

I took a go at the suggested refactoring in comment:9 at Phab:D3881.

comment:17 Changed 2 years ago by Ben Gamari <ben@…>

In 895a7650/ghc:

Refactor type family instance abstract syntax declarations

This implements @simonpj's suggested refactoring of the abstract syntax
for type/data family instances (from
https://ghc.haskell.org/trac/ghc/ticket/14131#comment:9). This combines
the previously separate `TyFamEqn` and `DataFamInstDecl` types into a
single `FamEqn` datatype. This also factors the `HsImplicitBndrs` out of
`HsTyPats` in favor of putting them just outside of `FamEqn` (as opposed
to before, where all of the implicit binders were embedded inside of
`TyFamEqn`/`DataFamInstDecl`). Finally, along the way I noticed that
`dfid_fvs` and `tfid_fvs` were completely unused, so I removed them.

Aside from some changes in parser test output, there is no change in
behavior.

Requires a Haddock submodule commit from my fork (at
https://github.com/RyanGlScott/haddock/commit/815d2deb9c0222c916becccf84
64b740c26255fd)

Test Plan: ./validate

Reviewers: simonpj, austin, goldfire, bgamari, alanz

Reviewed By: bgamari

Subscribers: mpickering, goldfire, rwbarton, thomie, simonpj

GHC Trac Issues: #14131

Differential Revision: https://phabricator.haskell.org/D3881

comment:18 Changed 2 years ago by bgamari

Owner: RyanGlScott deleted
Status: patchnew

I believe more work is needed to fix the actual bug here.

comment:19 in reply to:  18 Changed 2 years ago by RyanGlScott

Owner: set to RyanGlScott

Replying to bgamari:

I believe more work is needed to fix the actual bug here.

Indeed there is. I'll work on polishing up Phab:D3872 and fixing this ticket for good.

comment:20 Changed 2 years ago by RyanGlScott

Status: newpatch

Phab:D3872 is ready for review.

comment:21 Changed 2 years ago by RyanGlScott

Blocked By: 13988 added

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

In 0829821a/ghc:

Implicitly bind kind variables in type family instance RHSes when it's sensible

Summary:
Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:

```lang=haskell
type T = (Nothing :: Maybe a)
```

However, it would not accept a very similar type family instance:

```lang=haskell
type family   T :: Maybe a
type instance T = (Nothing :: Maybe a)
```

The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing #14131.

In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be //implicitly// bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in #7938 and #9574 to typecheck, whereas before they would
have been rejected.

Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
undergone a minor facelift).

While doing this has the upside of fixing #14131, it also made it easier to
trigger #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

GHC Trac Issues: #13985, #14131

Differential Revision: https://phabricator.haskell.org/D3872

comment:23 Changed 2 years ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: indexed-types/should_compile/T14131
Note: See TracTickets for help on using tickets.