#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 Revisions:

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: Changed 17 months ago by simonpj

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

comment:2 Changed 17 months ago by jstolarek

  • Owner set to jstolarek

comment:3 Changed 17 months 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 17 months ago by jstolarek

  • Description modified (diff)

comment:5 in reply to: ↑ 1 Changed 17 months 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 17 months 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 16 months 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 16 months 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 16 months ago by jstolarek

Ok, I'll try that.

comment:10 Changed 16 months 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 16 months 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 16 months 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 16 months ago by Jan Stolarek <jan.stolarek@…>

In 1d2ffb6ab1ef973c85f893b5ea4a72cfa59ce484/ghc:

Validate inferred theta. Fixes #8883

This checks that all the required extensions are enabled for the
inferred type signature.

Updates binary and vector submodules.

comment:14 Changed 16 months ago by jstolarek

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_fail/T8883

comment:15 Changed 16 months 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.

Last edited 16 months ago by Lemming (previous) (diff)

comment:16 Changed 16 months 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: Changed 16 months 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:19 in reply to: ↑ 17 Changed 16 months 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 14 months ago by simonpj

See more fallout in #9190

comment:21 Changed 14 months ago by Simon Peyton Jones <simonpj@…>

In 56f8777f99d9fd849ca6f1151fead3f62707f308/ghc:

Improve error message in Trac #8883

The improvement is to report the inferred type in the error message,
as suggested in email on ghc-deves (10 Jun 14).

comment:22 Changed 14 months 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 14 months ago by jstolarek

  • Owner set to jstolarek

comment:24 Changed 13 months ago by Jan Stolarek <jan.stolarek@…>

In d5c6fd6c8525477f869d62d5c71945672b46ee56/ghc:

Document #8883 in the release notes

comment:25 Changed 13 months ago by jstolarek

  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.