Skip to content

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
Edited by Jan Stolarek
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information