Opened 3 years ago
Closed 3 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 )
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
comment:2 Changed 3 years ago by
Owner: | set to jstolarek |
---|
comment:3 Changed 3 years ago by
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
Description: | modified (diff) |
---|
comment:5 Changed 3 years ago by
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
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
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
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:10 Changed 3 years ago by
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
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
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:14 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → typecheck/should_fail/T8883 |
comment:15 Changed 3 years ago by
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
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
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:19 Changed 3 years ago by
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:22 Changed 3 years ago by
Owner: | jstolarek deleted |
---|---|
Resolution: | fixed |
Status: | closed → new |
Re-opening this as a reminder to mention this in the release notes.
comment:23 Changed 3 years ago by
Owner: | set to jstolarek |
---|
comment:25 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | new → 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