#14579 closed bug (fixed)
GeneralizedNewtypeDeriving produces ambiguously-kinded code
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.10.1 |
Component: | Compiler (Type checker) | Version: | 8.2.2 |
Keywords: | deriving | Cc: | mnguyen |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | deriving/should_compile/T14579{a,b} |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | Phab:D4264, Phab:D5229, https://gitlab.haskell.org/ghc/ghc/merge_requests/261 | |
Wiki Page: |
Description
This program should compile:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a)) deriving Eq
After all, it should produce this Eq (Glurp a)
instance, which compiles without issue:
instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat ('Proxy :: Proxy a) -> Wat ('Proxy :: Proxy a) -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
But despite my wishful thinking, GHC does not actually do this. In fact, the code that GHC tries to generate for an Eq (Glurp a)
instance is completely wrong:
$ /opt/ghc/8.2.2/bin/ghci -ddump-deriv Bug.hs GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance forall a (x :: Data.Proxy.Proxy a). GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Wat x) where (GHC.Classes.==) = GHC.Prim.coerce @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool) @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool) (GHC.Classes.==) (GHC.Classes./=) = GHC.Prim.coerce @(GHC.Base.Maybe a_a2wE -> GHC.Base.Maybe a_a2wE -> GHC.Types.Bool) @(Bug.Wat x_a2wF -> Bug.Wat x_a2wF -> GHC.Types.Bool) (GHC.Classes./=) instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where (GHC.Classes.==) = GHC.Prim.coerce @(Bug.Wat Data.Proxy.Proxy -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool) @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool) (GHC.Classes.==) (GHC.Classes./=) = GHC.Prim.coerce @(Bug.Wat Data.Proxy.Proxy -> Bug.Wat Data.Proxy.Proxy -> GHC.Types.Bool) @(Bug.Glurp a_a1vT -> Bug.Glurp a_a1vT -> GHC.Types.Bool) (GHC.Classes./=) Derived type family instances: Bug.hs:12:12: error: • Couldn't match representation of type ‘a0’ with that of ‘a’ arising from a use of ‘GHC.Prim.coerce’ ‘a’ is a rigid type variable bound by the instance declaration at Bug.hs:12:12-13 • In the expression: GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==) In an equation for ‘==’: (==) = GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==) When typechecking the code for ‘==’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‘Eq (Glurp a)’ • Relevant bindings include (==) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12) | 12 | deriving Eq | ^^ Bug.hs:12:12: error: • Could not deduce (Eq a0) arising from a use of ‘==’ from the context: Eq a bound by the instance declaration at Bug.hs:12:12-13 The type variable ‘a0’ is ambiguous These potential instances exist: instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’ instance Eq Ordering -- Defined in ‘GHC.Classes’ instance Eq Integer -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’ ...plus 25 others ...plus 9 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the third argument of ‘GHC.Prim.coerce’, namely ‘(==)’ In the expression: GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==) In an equation for ‘==’: (==) = GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==) When typechecking the code for ‘==’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv | 12 | deriving Eq | ^^ Bug.hs:12:12: error: • Couldn't match representation of type ‘a1’ with that of ‘a’ arising from a use of ‘GHC.Prim.coerce’ ‘a’ is a rigid type variable bound by the instance declaration at Bug.hs:12:12-13 • In the expression: GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (/=) In an equation for ‘/=’: (/=) = GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (/=) When typechecking the code for ‘/=’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‘Eq (Glurp a)’ • Relevant bindings include (/=) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:12:12) | 12 | deriving Eq | ^^ Bug.hs:12:12: error: • Could not deduce (Eq a1) arising from a use of ‘/=’ from the context: Eq a bound by the instance declaration at Bug.hs:12:12-13 The type variable ‘a1’ is ambiguous These potential instances exist: instance forall k (s :: k). Eq (Proxy s) -- Defined in ‘Data.Proxy’ instance Eq Ordering -- Defined in ‘GHC.Classes’ instance Eq Integer -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’ ...plus 25 others ...plus 9 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the third argument of ‘GHC.Prim.coerce’, namely ‘(/=)’ In the expression: GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (/=) In an equation for ‘/=’: (/=) = GHC.Prim.coerce @(Wat Proxy -> Wat Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (/=) When typechecking the code for ‘/=’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv | 12 | deriving Eq | ^^
Yikes. To see what went wrong, let's zoom in a particular part of the -ddump-deriv
output (cleaned up a bit for presentation purposes):
instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat 'Proxy -> Wat 'Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
Notice that it's Wat 'Proxy
, and not Wat ('Proxy :: Proxy a)
! And no, that's not just a result of GHC omitting the kind information—you will see the exact same thing if you compile with -fprint-explicit-kinds
. What's going on here?
As it turns out, the types inside of those visible type applications aren't Type
s, but rather HsType GhcRn
s (i.e., source syntax). So what is happening is that GHC is literally producing @(Wat 'Proxy -> Wat 'Proxy -> Bool)
as source syntax, not as a Type
. This means that 'Proxy
has an underspecified kind, resulting in the numerous The type variable ‘a0’ is ambiguous
errors you see above.
Change History (28)
comment:1 Changed 21 months ago by
comment:2 Changed 21 months ago by
Differential Rev(s): | → Phab:D4264 |
---|---|
Status: | new → patch |
comment:3 Changed 21 months ago by
What change to typeToHsType
do we want? The problem is to specify the invisible kind arguments to occurrences of poly-kinded type-constructor applications. Eg
instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat 'Proxy -> Wat 'Proxy -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
The problem is the invisible kind arguments to the poly-kinded 'Proxy
occurrences. If we had visible kind application we could use that, but we don't. Solution: add a kind signature, as in the Description:
instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat ('Proxy :: Proxy a) -> Wat ('Proxy :: Proxy a) -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
When do we need a kind signature?
- (a) When we have an application of a type constructor with invisible arguments
- (b) And the invisible arguments are not fixed by the kinds of the visible arguments.
Probably just using (a) is enough to reduce the noise of redundant kind signatures to reasonable levels.
comment:4 Changed 21 months ago by
Is there any reason we can't say
typeToLHsType = noLoc . HsCoreTy
? That certainly seems to save a lot of huffing and puffing.
comment:5 Changed 21 months ago by
Good thought. But these types have free type variables, bound by the instance decl. I'm far from sure they'd line up right.
comment:6 Changed 21 months ago by
simonpj's hunch appears to be right—I just attempted to compile GHC with goldfire's suggested change, and wound up face-first in panictown:
libraries/base/GHC/Generics.hs:811:13: error:ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.5.20171213 for x86_64-unknown-linux): No skolem info: [p3_a3Jl] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:2892:5 in ghc:TcErrors
I'll try simonpj's suggested refactoring in comment:3.
comment:7 Changed 21 months ago by
Ryan's visit to panictown notwithstanding, I'm still not convinced by comment:5. comment:5 seems to be suggesting that we need the generated code to pass through the renamer, so that the type variables can be captured. This is a reasonable guess. But typeToLHsType
, as currently written (and working), uses Exact
names, so the journey through the renamer doesn't capture anything. Perhaps the panic is actually caused by these lines in RnTypes:
rnHsTyKi _ (HsCoreTy ty) = return (HsCoreTy ty, emptyFVs) -- The emptyFVs probably isn't quite right -- but I don't think it matters
Maybe it matters. Or maybe I'm missing something more fundamental.
comment:8 Changed 21 months ago by
I think it would be worthwhile to investigate this issue further (probably in another Trac ticket). My gut feeling is that Phab:D4264 is simple enough that we can adopt it without too much worry—worst comes to worst, we can scrap the current implementation of typeToLHsType
in favor of something simpler later.
comment:10 Changed 21 months ago by
Milestone: | → 8.4.1 |
---|---|
Status: | patch → merge |
Test Case: | → deriving/should_compile/T14579 |
Could merge to 8.4.1 if convenient.
comment:11 Changed 20 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged in ebf8e07629.
comment:12 follow-up: 16 Changed 11 months ago by
Blocked By: | 12045 added |
---|---|
Milestone: | 8.4.1 → 8.8.1 |
Resolution: | fixed |
Status: | closed → new |
I wonder if the hack we implemented to fix this issue originally could be made substantially simpler with visible kind applications (which should be available soon-ish). With VKAs, we could instead generate the following code:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a)) instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
I'll reopen this ticket to keep track of this idea.
comment:13 Changed 11 months ago by
Yes indeed. comment:3 identifies VKA as the desired facility, with kind signatures as second best. Good idea to re-open
comment:14 Changed 11 months ago by
Cc: | mynguyen added |
---|
Cc'ing the implementor of visible kind application.
comment:15 Changed 11 months ago by
Cc: | mnguyen added; mynguyen removed |
---|
comment:16 Changed 10 months ago by
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a)) instance Eq a => Eq (Glurp a) where (==) = coerce @(Wat ('Proxy @a) -> Wat ('Proxy @a) -> Bool) @(Glurp a -> Glurp a -> Bool) (==)
I try this with my current VKA and it fails
T14579a.hs:15:32: error: Not in scope: type variable ‘a’ T14579a.hs:15:51: error: Not in scope: type variable ‘a’ T14579a.hs:16:25: error: Not in scope: type variable ‘a’ T14579a.hs:16:44: error: Not in scope: type variable ‘a’
???
comment:17 Changed 10 months ago by
I've responded to comment:16 at https://phabricator.haskell.org/D5229#inline-42631. (The code is very nearly correct; you just need some minor tweaks to make it compile).
Also, thanks for adding a test case for this! Once the VKA patch lands, I can look into tweaking GeneralizedNewtypeDeriving
itself such that it generates code with visible kind applications.
comment:18 Changed 9 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
comment:19 Changed 9 months ago by
Differential Rev(s): | Phab:D4264 → Phab:D4264, Phab:D5229 |
---|---|
Test Case: | deriving/should_compile/T14579 → deriving/should_compile/T14579{a} |
A test case was added in 17bd163566153babbf51adaff8397f948ae363ca:
Author: mynguyen <mnguyen1@brynmawr.edu> Date: Tue Dec 18 11:52:26 2018 -0500 Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229
To ensure that the code in comment:12 actually typechecks. However, the task of making GeneralizedNewtypeDeriving
actually generate this code remains to be done.
comment:20 Changed 9 months ago by
When writing comment:12, I was originally hopeful that we could scrap all of commit 649e777211fe08432900093002547d7358f92d82—that is, that we could avoid generating any explicit kind signatures and exclusively use visible kind application. Alas, this is not the case. Consider this tortuous example:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE PolyKinds #-} module Bug where import Data.Kind import Data.Proxy -- type P :: forall {k} {t :: k}. Proxy t type P = 'Proxy -- type Wat :: forall a. Proxy a -> * newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a) deriving Eq -- type Wat2 :: forall {a}. Proxy a -> * type Wat2 = Wat -- type Glurp :: * -> * newtype Glurp a = MkGlurp (Wat2 (P :: Proxy a)) deriving Eq
This compiles with GHC 8.6.3. However, if I try to switch GeneralizedNewtypeDeriving
over to using exclusively visible kind applications, then the code that it generates no longer compiles:
$ ghc/inplace/bin/ghc-stage2 Bug.hs -ddump-deriv [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ==================== Derived instances ==================== Derived class instances: instance forall a (x :: Data.Proxy.Proxy a). GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Wat x) where (GHC.Classes.==) = GHC.Prim.coerce @(GHC.Maybe.Maybe a_a1wk -> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool) @(Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool) ((GHC.Classes.==) @(GHC.Maybe.Maybe a_a1wk)) :: Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool (GHC.Classes./=) = GHC.Prim.coerce @(GHC.Maybe.Maybe a_a1wk -> GHC.Maybe.Maybe a_a1wk -> GHC.Types.Bool) @(Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool) ((GHC.Classes./=) @(GHC.Maybe.Maybe a_a1wk)) :: Bug.Wat @a_a1wk x_a210 -> Bug.Wat @a_a1wk x_a210 -> GHC.Types.Bool instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where (GHC.Classes.==) = GHC.Prim.coerce @(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool) @(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool) ((GHC.Classes.==) @(Bug.Wat2 Bug.P)) :: Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool (GHC.Classes./=) = GHC.Prim.coerce @(Bug.Wat2 Bug.P -> Bug.Wat2 Bug.P -> GHC.Types.Bool) @(Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool) ((GHC.Classes./=) @(Bug.Wat2 Bug.P)) :: Bug.Glurp a_avE -> Bug.Glurp a_avE -> GHC.Types.Bool Derived type family instances: Bug.hs:21:12: error: • Couldn't match representation of type ‘a0’ with that of ‘a’ arising from a use of ‘GHC.Prim.coerce’ ‘a’ is a rigid type variable bound by the instance declaration at Bug.hs:21:12-13 • In the expression: GHC.Prim.coerce @(Wat2 P -> Wat2 P -> Bool) @(Glurp a -> Glurp a -> Bool) ((==) @(Wat2 P)) :: Glurp a -> Glurp a -> Bool In an equation for ‘==’: (==) = GHC.Prim.coerce @(Wat2 P -> Wat2 P -> Bool) @(Glurp a -> Glurp a -> Bool) ((==) @(Wat2 P)) :: Glurp a -> Glurp a -> Bool When typechecking the code for ‘==’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‘Eq (Glurp a)’ • Relevant bindings include (==) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:21:12) | 21 | deriving Eq | ^^ Bug.hs:21:12: error: • Couldn't match representation of type ‘a1’ with that of ‘a’ arising from a use of ‘GHC.Prim.coerce’ ‘a’ is a rigid type variable bound by the instance declaration at Bug.hs:21:12-13 • In the expression: GHC.Prim.coerce @(Wat2 P -> Wat2 P -> Bool) @(Glurp a -> Glurp a -> Bool) ((/=) @(Wat2 P)) :: Glurp a -> Glurp a -> Bool In an equation for ‘/=’: (/=) = GHC.Prim.coerce @(Wat2 P -> Wat2 P -> Bool) @(Glurp a -> Glurp a -> Bool) ((/=) @(Wat2 P)) :: Glurp a -> Glurp a -> Bool When typechecking the code for ‘/=’ in a derived instance for ‘Eq (Glurp a)’: To see the code I am typechecking, use -ddump-deriv In the instance declaration for ‘Eq (Glurp a)’ • Relevant bindings include (/=) :: Glurp a -> Glurp a -> Bool (bound at Bug.hs:21:12) | 21 | deriving Eq | ^^
Ambiguity once again rears its ugly head. You might be tempted to think that we could sprinkle @a
somewhere in Wat2 P
to resolve the ambiguity, but this is impossible, as all of the type variable binders in Wat2
and P
are inferred, making them unavailable for visible kind application. The only way out of this mess is to surround P
with an explicit kind signature (i.e., (P :: Proxy a)
).
That being said, visible kind application will help us quite a bit, as we can avoid generating explicit kind signatures whenever a tycon only has specified or required type variable binders in its kind. But we'll still need to keep around the hack in commit 649e777211fe08432900093002547d7358f92d82 in the event that there are any inferred type variables.
comment:21 Changed 9 months ago by
Cruelly enough, comment:20 means the the original program in this ticket must have an explicit kind signature anyway, since in the kind of 'Proxy
:
'Proxy :: forall {k} (a :: k). Proxy a
We have an inferred type variable binder! Argh.
I wonder if we can be a bit smarter about where we put explicit kind signatures? This is the code that GHC 8.6.3 currently generates for the original program's Eq (Glurp a)
instance:
instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where (GHC.Classes.==) = GHC.Prim.coerce @((Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep) -> (Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep) -> GHC.Types.Bool) @(Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool) (GHC.Classes.==) :: Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool (GHC.Classes./=) = GHC.Prim.coerce @((Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep) -> (Bug.Wat (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: TYPE GHC.Types.LiftedRep)) :: TYPE GHC.Types.LiftedRep) -> GHC.Types.Bool) @(Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool) (GHC.Classes./=) :: Bug.Glurp a_a1Dx -> Bug.Glurp a_a1Dx -> GHC.Types.Bool
There are many explicit kind signatures here that are completely redundant—for instance, each (_ :: TYPE GHC.Types.LiftedRep)
signature is redundant, since they're not needed to fix any type variables. The only signature that's strictly necessary is the (Data.Proxy.Proxy :: (Data.Proxy.Proxy a_a1Dx :: ...))
one, since that fixes a_a1Dx
.
Perhaps we should adopt a more fine-grained heuristic (besides the mere presence of inferred type variable binders) to determine when to insert explicit kind signatures? For instance, the reify_tc_app
function in TcSplice
(which reifies applications of tycons) uses a more complicated heuristic: if the free variables of the tycon's kind are not a subset of the free variables of the arguments in injective positions, then it needs an explicit signature. (This is explained in this Note).
This heuristic could work well in this situation as well. We'd need to modify the definition of "injective positions" to include specified arguments (currently it only includes required ones), but if we did, then I believe we could drop all of the explicit signatures in the original program.
comment:22 Changed 8 months ago by
I was originally hopeful that we could avoid generating any explicit kind signatures and exclusively use visible kind application.
Yes I agree with your analysis. Visible kind application (VKA) can only be used for Specified arguments, and user-defined types can have Inferred arguments. So yes, if there are no Inferred ones (a common case) you can use VKA; but not if not. Annoying!
comment:23 Changed 8 months ago by
Blocked By: | 12045 removed |
---|
To recap, there are two distinct-but-related tasks here:
- Make GND-generated code use VKA to instantiate arguments in specified positions.
- Minimize the number of explicit kind signatures generated by GND code by using the approach discussed in comment:21.
Althought (1) and (2) can technically be done independently, it's only the combination of the two that will make it so that the original program in this ticket generate code with no explicit kind signatures adorning its 'Proxy
types. I'll look into this approach.
comment:24 Changed 8 months ago by
Differential Rev(s): | Phab:D4264, Phab:D5229 → Phab:D4264, Phab:D5229, https://gitlab.haskell.org/ghc/ghc/merge_requests/261 |
---|---|
Status: | new → patch |
comment:25 Changed 8 months ago by
To be clear
- Phab:D4264 has landed (comment:9)
- Phab:D5229 has landed (comment:19)
So the only remaining issue is MR 261 "Fix #14579 by defining tyConAppNeedsKindSig, and using it"
comment:26 Changed 8 months ago by
I've read the patch, but I'm commenting here because Trac has greater longevity than code reviews.
You have written a commendably detailed Note -- thank you. Still, it took me a solid hour of head-scratching to really understand it. Here are some thoughts that may (or may not) help to make it clearer.
First, it took me ages reslise that tyConAppNeedsKindSig
can
be done without knowing the actual arguments to T
. Only once
I'd realised that did I discover that, sure enough, it doesn't rely
on args
, only on length args
! So I strongly suggest
tyConAppNeedsKindSig :: Bool -- ^ Should specified binders count towards injective positions in -- the kind of the TyCon? -> TyCon -> Int -- Number of args -> Bool -- Does (T t1 .. tn) need a signature tyConAppNeedsKindSig spec_inj_pos tc n_args = ...
That is, pass the number of args, not the actual args.
That makes it clear that the function could, in principle, live in
TyCon
. It could even be cached in the TyCon, as a list of Bools
or, because
of the Inferred/Specified thing, two lists of Bools
. But the caching
is probably not worth it.
Ok then, my thought process went like this. Given a application
T t1 .. tn
, does it need a kind signature? Why might it need a kind
signature? So that we can fill in any of T's omitted arguments. By
an "omitted argument" I mean one that we do not reify expicitly in the
HsType
. Sometimes the omitted ones are Inferred ones (in
typeToHsType
); sometimes both Inferred and Specified (in
TcSplice
); but the key thing is that they don't appear in the
HsType
.
What do we mean by "fill in"? Suppose
T :: forall {k}. Type -> (k->*) -> k
and we have the application T {j} Int aty
. When we convert to
HsType
we are going to omit the inferred arg {j}
. Is it fixed
by the other non-inferred args? Yes: if we know the kind of aty :: blah
,
we'll generate an equality constraint (kappa->*) ~ blah
and, assuming
we can solve it, that will fix kappa
. (Here kappa
is the unification
variable that we instantiate k
with.)
So the question becomes this.
- Consider the first
n
args of T: do the kinds of the non-omitted arguments determine the omitted arguments?
We'll only handle the case were the omitted arguments are NamedTCB
,
so we need to determine a variable.
When does a kind "determine" a variable? This is what injectiveVarsOfType
computes.
-- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation -- of what an injective position is.) injectiveVarsOfType :: Type -> FV
Rather than speak of "injective positions" I think of it like this:
if a
is in injectiveVarsOfType ty
then knowing ty
fixes, or determines, a
.
More formally:
If a is in (injectiveVarsOfType ty) and S1(ty) ~ S2(ty) then S1(a) ~ S2(a) where S1 and S2 are arbitrary substitutions
For example, if F
is a non-injective type family, then
injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
(This part about injectiveVarsOfType
is not new -- but I'd suggest
adding it as comments to the function.)
So we can refine the question:
- Consider the first
n
args of T, and each omitted argumenti <= n
: is argumenti
aNamedTCB
binderb
, and doesb
appear ininjectiveVarsOfTtype (k(i+1) .. k(n))
? Wherekj
is the kind of the j'th argument of T.
Much of this is as you have it, except that I'm not lookin at result_kind
(in your tyConAppNeedsKindSig
.
If I can't fill in all omitted arguments, I'll add a kind signature. So for a silly thing like
T :: forall k. Type -> Type
and the type (T {j} Int)
, I'll add a kind signature, which actually does no good since k
is unused.
But it's a silly example. And you'll add one for a different silly example.
T :: forall k. Type -> F k
which equally does no good.
Nothing here is radically different from what you have. But I find the chain of thought here easier to follow.
comment:27 Changed 7 months ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
Test Case: | deriving/should_compile/T14579{a} → deriving/should_compile/T14579{a,b} |
This was finally fixed in e88e083d62389d5c8d082a25395a3d933ab2f03b.
Hm... look at
TcGenDeriv.nlHsAppType
. Presumably you want to add the necessary kind signatures when doingtypeToHsType
.