[GHC] #8883: FlexibleContexts checking should happen also on inferred signature

[GHC]

#8883: FlexibleContexts checking should happen also on inferred signature
------------------------------------+-------------------------------------
       Reporter:  Blaisorblade      |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.6.3
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 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>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler