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

[GHC]

#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