#8883: FlexibleContexts checking should happen also on inferred signature -------------------------------------+------------------------------------ Reporter: Blaisorblade | Owner: jstolarek Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by jstolarek: Old description:
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.
{{{#!haskell {-# 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 }}}
New description: 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. {{{#!haskell {-# 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 }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8883#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler