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
Cc: | RyanGlScott added |
---|---|
Keywords: | TypeFamilies added |
comment:2 Changed 2 years ago by
comment:3 Changed 2 years ago by
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
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 follow-up: 6 Changed 2 years ago by
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 Changed 2 years ago by
Differential Rev(s): | → Phab:D3872 |
---|---|
Related Tickets: | → #13985 |
Status: | new → patch |
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
Related Tickets: | #13985 → #7938, #9574, #13985 |
---|
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
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.
comment:9 follow-up: 10 Changed 2 years ago by
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 Changed 2 years ago by
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 follow-up: 12 Changed 2 years ago by
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 Changed 2 years ago by
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 follow-up: 14 Changed 2 years ago by
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 Changed 2 years ago by
Replying to simonpj:
Really?
reportFloatingKvs
seems to report variables mentioned intypat_tvs
, which doesn't look like the ones on the RHS. I wasn't expecting a test intcFamTyPats
, but rather intcTyFamInstEqn
.
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
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 theHsTyPats
includes (via the renamer) the variables mentioned in the RHS. You arrange thattc_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
Differential Rev(s): | Phab:D3872 → Phab:D3872, Phab:D3881 |
---|
I took a go at the suggested refactoring in comment:9 at Phab:D3881.
comment:18 follow-up: 19 Changed 2 years ago by
Owner: | RyanGlScott deleted |
---|---|
Status: | patch → new |
I believe more work is needed to fix the actual bug here.
comment:19 Changed 2 years ago by
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:21 Changed 2 years ago by
Blocked By: | 13988 added |
---|
comment:23 Changed 2 years ago by
Milestone: | → 8.4.1 |
---|---|
Resolution: | → fixed |
Status: | patch → closed |
Test Case: | → indexed-types/should_compile/T14131 |
No. Not really related to #12369. Perhaps related to #13985. Perhaps not.