Opened 3 years ago
Closed 2 years ago
#8883 closed bug (fixed)
FlexibleContexts checking should happen also on inferred signature
Reported by: | Blaisorblade | Owned by: | jstolarek |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.6.3 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_fail/T8883 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by jstolarek)
I assume that if a program typechecks, adding any missing top-level signature inferred by GHC should be a meaning-preserving transformation and yield a new program which typechecks. (Please correct me if I'm wrong). But I've found a violation: namely, given enough other extensions (I think TypeFamilies is the relevant one), GHC will infer signatures which would require FlexibleContexts! Arguably, either those signatures should be rejected in the first place with a special error message (since GHC is not supposed to show code the user didn't write in error messages), or TypeFamilies should imply FlexibleContexts (or a restricted form which is sufficient for what TypeFamilies produces - namely, constraints can contain type families in place of raw type variables).
Here's an example - without FlexibleContexts it does not typecheck , unless you comment out the signature of fold and unfold. Those signatures where produced by GHCi (with :browse) in the first-place.
{-# LANGUAGE TypeFamilies, DeriveFunctor, NoMonomorphismRestriction #-} -- , FlexibleContexts data Fix f = In { out :: f (Fix f) } data Expr = Const Int | Add Expr Expr data PFExpr r = ConstF Int | AddF r r deriving Functor type Expr' = Fix PFExpr class Regular0 a where deepFrom0 :: a -> Fix (PF a) deepTo0 :: Fix (PF a) -> a type family PF a :: * -> * type instance PF Expr = PFExpr instance Regular0 Expr where deepFrom0 = In . (\expr -> case expr of Const n -> ConstF n Add a b -> AddF (deepFrom0 a) (deepFrom0 b)) deepTo0 = (\expr' -> case expr' of ConstF n -> Const n AddF a b -> Add (deepTo0 a) (deepTo0 b)) . out class Regular a where from :: a -> PF a a to :: PF a a -> a instance Regular Expr where from expr = case expr of Const n -> ConstF n Add a b -> AddF a b to expr' = case expr' of ConstF n -> Const n AddF a b -> Add a b -- But in fact, the construction is just an instance of fold. fold :: (Functor (PF a), Regular a) => (PF a b -> b) -> a -> b unfold :: (Functor (PF b), Regular b) => (a -> PF b a) -> a -> b fold f = f . fmap (fold f) . from unfold f = to . fmap (unfold f) . f
Change History (25)
comment:1 follow-up: ↓ 5 Changed 3 years ago by simonpj
comment:2 Changed 3 years ago by jstolarek
- Owner set to jstolarek
comment:3 Changed 3 years ago by Blaisorblade
Thanks a lot for the prompt answer, and I agree on the priority. I only take the time to report such bugs because GHC is so good ;-)
comment:4 Changed 3 years ago by jstolarek
- Description modified (diff)
comment:5 in reply to: ↑ 1 Changed 3 years ago by jstolarek
Replying to simonpj:
if someone would like to have a go it would not be hard and I could offer guidance.
I'd like to tackle this one. Guidance will be really appreciated.
I reduced the test case to this snippet of code:
{-# LANGUAGE TypeFamilies, DeriveFunctor, NoMonomorphismRestriction #-} -- , FlexibleContexts module T8883 where type family PF a :: * -> * class Regular a where from :: a -> PF a a -- But in fact, the construction is just an instance of fold. --fold :: (Functor (PF a), Regular a) => (PF a b -> b) -> a -> b fold f = f . fmap (fold f) . from
So how should GHC behave for this code? Reject it because FlexibleContexts extension is not enabled?
comment:6 Changed 3 years ago by simonpj
I suppose that it should reject it because FlexibleContexts is not enabled, with an error message that suggests it.
Simon
comment:7 Changed 3 years ago by jstolarek
I finally had some time to look into this one. I traced what happens when the type signature is present and when it has to be inferred. I see what is the flow of control in both cases, but I don't understand details of type inference itself. From what I've observed in the latter case type signature for fold is inferred in tcPolyKind by calling simplifyInfer (in TcBinds.lhs). The question is whether the missing language extension should be detected *during* type inference or *after* type inference?
comment:8 Changed 3 years ago by simonpj
I suppose that tcPolyInfer could check the returned theta, and ensure that it satisfies the rules for inflexible contexts, unless FlexibleContexts is enabled?
Simon
comment:9 Changed 3 years ago by jstolarek
Ok, I'll try that.
comment:10 Changed 3 years ago by jstolarek
Inserting a call to checkValidTheta after the theta has been zonked (in tcPolyInfer) indeed does the job but I can't solve one problem. checkValidTheta requires UserTypeCtxt parameter. I assume that in this case the value should be InfSigCtxt, since we are dealing with inferred signature. The problem is that InfSigCtxt requires name of function for which the type has been inferred. This information doesn't seem to be easily available inside tcPolyInfer. I noticed that the name is stored inside name_taus so I did a hack that calls checkValidTheta (InfSigCtxt (fst . head $ name_taus)) theta. In this particular case it works because fold name is stored as first in the list. But I don't know what is a general solution for finding name of function for which we are inferring the signature.
comment:11 Changed 3 years ago by simonpj
Well if you have
f x = g x g x = f (h x)
then tcPolyInfer will be called on the two bindings together. If you happened to get a badly-shaped inferred theta, do you want to report an error for f, or for g, or both? I think just one would do, which is what you have implemented. If you want one per function, put the check in mkExport instead. Either way it's not a big deal.
Comments, with an example, would be a Good Thing.
Simon
comment:12 Changed 3 years ago by jstolarek
Before I push my patches let me remark that this is a breaking change. There were files in the main source code as well as boot libraries that required enabling either FlexibleContexts or TypeFamilies extensions (or both). Error messages are informative so it's easy to fix the code, but when we release GHC 7.10 some user libraries will need to adjust to this change.
comment:13 Changed 3 years ago by Jan Stolarek <jan.stolarek@…>
comment:14 Changed 3 years ago by jstolarek
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to typecheck/should_fail/T8883
comment:15 Changed 3 years ago by Lemming
You can rewrite the constraint
(Functor (PF a), Regular a)
to
(PF a ~ pfa, Functor pfa, Regular a)
and then it is no longer a FlexibleContext. However, this trick does not work in superclasses since you must only use class parameters there and you cannot introduce new variables.
comment:16 Changed 3 years ago by rwbarton
If we're doing this, can we also enable FlexibleContexts by default? Is there any good reason not to? (Can it break any working code?)
comment:17 follow-up: ↓ 19 Changed 3 years ago by simonpj
Lemming has a good point, I guess. Functor (PF a) is currently rejected without FlexibleContexts but I guess it could instead be accepted. Moreover even in H98 the context Functor (f a) is accepted, so you could argue that with TypeFamilies we should accept Functor (PF a).
I can't get terribly excited about this decision; but I can see the logic, and I'll gladly change the current behaviour if there is support for doing so. (This would affect both inferred and declared types, of course.)
rwbarton: GHC does Haskell 2010 by default. That's how we choose what to enable by default, otherwise we'd argue about "should X be on by default" for ages!
Simon
comment:18 Changed 3 years ago by simonpj
comment:19 in reply to: ↑ 17 Changed 3 years ago by Lemming
Replying to simonpj:
I can't get terribly excited about this decision; but I can see the logic, and I'll gladly change the current behaviour if there is support for doing so. (This would affect both inferred and declared types, of course.)
As I said, you cannot eliminate all FlexibleContexts using an auxiliary variable. You cannot convert class (Functor (PF a)) => C a where to class (Functor b, b ~ PF a) => C a where because you cannot introduce the variable b in the superclass constraint.
Thus features provided by FlexibleContexts cannot always be achieved by TypeFamilies, and thus FlexibleContexts should not be a "superfeature" of TypeFamilies.
comment:20 Changed 2 years ago by simonpj
See more fallout in #9190
comment:21 Changed 2 years ago by Simon Peyton Jones <simonpj@…>
comment:22 Changed 2 years ago by jstolarek
- Owner jstolarek deleted
- Resolution fixed deleted
- Status changed from closed to new
Re-opening this as a reminder to mention this in the release notes.
comment:23 Changed 2 years ago by jstolarek
- Owner set to jstolarek
comment:24 Changed 2 years ago by Jan Stolarek <jan.stolarek@…>
comment:25 Changed 2 years ago by jstolarek
- Resolution set to fixed
- Status changed from new to closed
You are technically quite right, and this wouldn't be hard to fix, by looking at the inferred type.
Not, perhaps, very high priority, but if someone would like to have a go it would not be hard and I could offer guidance.
Simon