FlexibleContexts checking should happen also on inferred signature
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