Opened 3 years ago

Closed 3 years ago

Last modified 22 months ago

#12670 closed bug (fixed)

Representation polymorphism validity check is too strict

Reported by: bgamari Owned by: goldfire
Priority: high Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: Typeable, LevityPolymorphism Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

As of 465c6c5d15f8fb54afb78408f3a79e75e74d2cd4 GHC rejects this program,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
module Hi where
import GHC.Exts
data TypeRep (a :: k) where
    TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2).
             TypeRep a
          -> TypeRep b
          -> TypeRep (a -> b)

Claiming that it has inappropriate polymorphism over RuntimeRep,

$ ghc hi2.hs
[1 of 1] Compiling Hi               ( hi2.hs, hi2.o )

hi2.hs:7:5: error:
    • A representation-polymorphic type is not allowed here:
        Type: a
        Kind: TYPE r1
    • In the definition of data constructor ‘TrFun’
      In the data type declaration for ‘TypeRep’

I suspect this check is unnecessarily strict since we never need to store a value of type a to represent TypeRep a at runtime.

Change History (21)

comment:1 Changed 3 years ago by goldfire

Yes, I suppose TcHsSyn.checkForRepresentationPolymorphism is a bit loose in its definition of what is representation polymorphic. It should look for the kind to be TYPE blah before proceeding.

Last edited 3 years ago by goldfire (previous) (diff)

comment:2 Changed 3 years ago by bgamari

Well, I'm not quite sure that is sufficient; afterall the kind of a in the above example indeed has the form TYPE blah.

Rather, it seems like we need some way of determining whether a particular RuntimeRep variable affects the runtime representation of a type. It would seem at first glance that given a function type, e.g. a -> b, we would want to check that the kinds of a and b both have no free RuntimeRep variables. I suspect this is the only check necessary. We can assume that applications of any other tycon to RuntimeRep variables is safe since the type has already been subject to the checkForRepresentationPolymorphism check. Consequently, we have already determined that none of the type's type arguments will affect its representation and therefore any well-kinded application is safe.

Therefore, I propose that checkForRepresentationPolymorphism is simply the following,

checkForRepresentationPolymorphism :: SDoc -> Type -> TcM ()
checkForRepresentationPolymorphism extra ty
  | Just (tc, tys) <- splitTyConApp_maybe ty
  , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc
  = mapM_ (checkForRepresentationPolymorphism extra) (dropRuntimeRepArgs tys)

  | tuple_rep || sum_rep
  = {- fail -}

  | (args, res) <- splitFunTys ty
  , not $ all is_safe_arrow_argument args
  = {- fail -}

  | otherwise
  = return ()
  where
    tuple_rep    = runtime_rep `eqType` unboxedTupleRepDataConTy
    sum_rep      = runtime_rep `eqType` unboxedSumRepDataConTy
    tuple_or_sum = text (if tuple_rep then "tuple" else "sum")

    ki          = typeKind ty
    runtime_rep = getRuntimeRepFromKind "check_type" ki
    is_safe_arrow_argument =
          isEmptyVarSet . tyCoVarsOfType
        . getRuntimeRepFromKind "check_type" . typeKind
Last edited 3 years ago by bgamari (previous) (diff)

comment:3 Changed 3 years ago by bgamari

It seems that the above validity check loosening would also require that the Core Linter be loosened a bit. Otherwise, we find that this program will typecheck yet then fail due to validity check errors,

module Hi where
import GHC.Exts

data Fingerprint = Fingerprint
data TyCon = TyCon

data TypeRep (a :: k) where
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
               Fingerprint
            -> TypeRep a
            -> TypeRep b
            -> TypeRep (a -> b)

data AppResult (t :: k) where
    App :: TypeRep a -> TypeRep b -> AppResult (a b)

splitApp :: TypeRep a -> Maybe (AppResult a)
splitApp (TrFun _ _ _)   = Nothing

The Core lint issues stem from the fact that we have number of (unused) coercion bindings in scope in the produced Core whose types fail the okArrowArgKind check performed by lintArrow. For instance,

splitApp :: forall k_a2Xm (a_a2VN :: k_a2Xm).
            TypeRep k_a2Xm a_a2VN -> Maybe (AppResult k_a2Xm a_a2VN)
splitApp =
  \ (@ k_a2Xu)
    (@ (a_a2Xv :: k_a2Xu))
    (ds_d37A :: TypeRep k_a2Xu a_a2Xv) ->
    case ds_d37A of wild_00
    { TrFun @ r1_a2Xx @ r2_a2Xy @ a_a2Xz @ b_a2XA
            cobox_a2XB cobox_a2XC
            ds_d37Y ds_d37Z ds_d380 ->
        ...
        let {
          cobox_a2XU :: ((a_a2Xv |> cobox_a2XB) :: *) ~# ((a_a2Xz -> b_a2XA) :: *)
          cobox_a2XU = CO: <a_a2Xv>_N |> cobox_a2XB ; cobox_a2XC } in
        ...

which produces,

<no location info>: warning:
    In the type ‘((a_a2Xv |> cobox_a2XB) :: *)
                 ~#
                 ((a_a2Xz -> b_a2XA) :: *)’
    Ill-kinded argument in type or kind ‘a_a2Xz -> b_a2XA’
    type or kind ‘a_a2Xz -> b_a2XA’ kind: TYPE r1_a2Xx

due to the fact that a_a2Xz has RuntimeRep-polymorphic kind TYPE r1_a2Xx.

comment:4 Changed 3 years ago by simonpj

I think my fix to #12668 may have fixed comment:3. Not certain.

comment:5 Changed 3 years ago by bgamari

Simonpj, which fix is this? I haven't seen a fix for #12668 yet; presumably it has yet to be merged?

comment:6 Changed 3 years ago by simonpj

I think I failed to push; will do tomorrow

comment:7 Changed 3 years ago by bgamari

The patch that Simon was referring to in comment:4 was eefe86d96d40697707c3ddfb9973a30a1897241f. Unfortunately this doesn't fix the issue which described by this ticket; the typechecker still rejects the program given in the ticket description.

Richard and I discussed this a few weeks ago and came to a solution which looks something like this,

  • compiler/typecheck/TcPatSyn.hs

    diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
    index 5c62121..62724c8 100644
    a b module TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl 
    1313  ) where
    1414
    1515import HsSyn
     16import TcHsSyn( checkForRepresentationPolymorphism )
    1617import TcPat
    1718import Type( mkTyVarBinders, mkEmptyTCvSubst
    1819           , tidyTyVarBinders, tidyTypes, tidyType )
    tc_patsyn_finish lname dir is_infix lpat' 
    312313             arg_tys    = tidyTypes env2 arg_tys'
    313314             pat_ty     = tidyType  env2 pat_ty'
    314315
     316       -- Check that the arguments aren't representationally polymorphic
     317       ; mapM_ (checkForRepresentationPolymorphism empty) arg_tys
     318
    315319       ; traceTc "tc_patsyn_finish {" $
    316320           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
    317321           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
  • compiler/typecheck/TcTyClsDecls.hs

    diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
    index c009bc9..9335676 100644
    a b checkValidDataCon dflags existential_ok tc con 
    22962296          -- Check all argument types for validity
    22972297        ; checkValidType ctxt (dataConUserType con)
    22982298
     2299          -- Check for representationally polymorphic fields
     2300        ; mapM_ (checkForRepresentationPolymorphism empty) (dataConOrigArgTys con)
     2301
    22992302          -- Extra checks for newtype data constructors
    23002303        ; when (isNewTyCon tc) (checkNewDataCon con)
    23012304
  • compiler/typecheck/TcValidity.hs

    diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
    index 6cc40a5..c9f3bda 100644
    a b check_type _ _ _ (TyVarTy _) = return () 
    487487
    488488check_type env ctxt rank (FunTy arg_ty res_ty)
    489489  = do  { check_type env ctxt arg_rank arg_ty
    490         ; when (representationPolymorphismForbidden ctxt) $
    491           checkForRepresentationPolymorphism empty arg_ty
    492490        ; check_type env ctxt res_rank res_ty }
    493491  where
    494492    (arg_rank, res_rank) = funArgResRank rank

Unfortunately this still doesn't fix the Core Lint issues that inevitably pop up when you try to use such a type.

comment:8 Changed 3 years ago by simonpj

I think our new paper Levity polymorphism shows how to fix this. Richard is working on the implementation.

Are you stuck on this?

Simon

comment:9 Changed 3 years ago by goldfire

The fix for this is in branch wip/T12819. But I haven't had time to tie the patch up with a bow on top (put tests in, re-validate, etc). Soon. Soon.

comment:10 Changed 3 years ago by bgamari

Are you stuck on this?

To an extent, yes I was. The problem is that I cannot really use the TRFun that we introduced if I define it as,

data TypeRep (a :: k) where
    TRFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1) (res :: TYPE r2).
             TypeRep arg -> TypeRep res -> TypeRep (arg -> res)
    ...

due to the overly strict representational polymorphism checks described in this ticket.

I thought would workaround would be to even further narrow the types represented by TypeRep. Namely, we only represent arrow types where both arg and res are of kind Type,

data TypeRep (a :: k) where
    TRFun :: forall arg res. TypeRep arg -> TypeRep res -> TypeRep (arg -> res)
    ...

However, this leads to trouble when implementing serialization,

putTypeRep :: TypeRep a -> Put
putTypeRep (TRCon a b c)   = putWord8 0 >> ...
putTypeRep (TRApp a b c)   = putWord8 1 >> ...
putTypeRep (TRFun arg res) = putWord8 2 >> putTypeRep arg >> putTypeRep res
...

getSomeTypeRep :: Get SomeTypeRep
getSomeTypeRep = do
    tag <- getWord8
    case tag of
      0 -> ...
      1 -> ...
      2 -> do arg <- getSomeTypeRep
              res <- getSomeTypeRep
              {- uh oh! We don't know the kinds of arg and res
                 yet TRFun expects types of kind Type -}
              return (TRFun arg res)

The trouble here is that, since we have dropped typeRepKind, we have no way of verifying during deserialization that arg and res indeed have kind Type.

However, it sounds like wip/T12819 should unstick me; if I'm not mistaken none of this should be problematic assuming we are able to represent arrows with arbitrary argument and result kinds.

Last edited 3 years ago by bgamari (previous) (diff)

comment:11 Changed 3 years ago by bgamari

It turns out that the lack of typeRepKind has one more unfortunate effect: Data.Dynamic.dynApply can no longer be safely implemented. The reason is that we have no means of verifying that the result type of the function being applied is of kind Type.

comment:12 Changed 3 years ago by bgamari

To put a finer point on the concern I raised in comment:11:

Consider this example,

data TypeRep (a :: k)

pattern Fun :: forall k k' (a :: k) (b :: k').
               a -> b -> TypeRep (a -> b)

-- As seen in "A reflection on types"
data Dynamic where
    Dyn :: TypeRep a -> a -> Dynamic

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApply (Dyn rf f) (Dyn rx x) = do
    Fun arg res <- pure rx
    Just HRefl <- eqTypeRep arg rx

    -- We now know that the argument types match up but what about the 
    -- result type?
    -- 
    -- In order to package up the result (f x) into a `Dyn` we must
    -- know that the its type is of kind *. However, we don't know 
    -- this since TypeRep's index is poly-kinded.
    --
    -- Consequently we really need to do this, which requires typeRepKind,
    Just HRefl <- eqTypeRep (typeRepKind res) (typeRep @Type)

    pure $ Dyn res (f x)


-- Consider this example...
f :: Int -> Int#
f (I# n#) = n#

df :: Dynamic
df = Dyn f

-- Here is an example of a use of Dynamic that would expose the issue in dynApply
uhOh :: Maybe Dynamic
uhOh = dynApply df (Dynamic (42::Int))
Version 0, edited 3 years ago by bgamari (next)

comment:13 Changed 3 years ago by simonpj

Very good point. We can't make Dyn res (f x) unless f x :: Type, I agree.

Let's see what Richard has to say.

What is Fun? You're referring to some code I can't see.

In any case, I'd remark that we don't necessarily need the full generality of typeRepKind; we only need to know the arguments to (->) when we take rx apart.

comment:14 in reply to:  13 Changed 3 years ago by goldfire

Replying to simonpj:

Let's see what Richard has to say.

I say "yes".

I also say that your Fun is quite wrong. I prefer this one:

pattern Fun
  :: forall k (a_to_b :: k). ()
  => forall r r' (a :: TYPE r) (b :: TYPE r'). (k ~ Type, a_to_b ~ (a -> b)) 
  => TypeRep a -> TypeRep b -> TypeRep a_to_b

But otherwise I agree with your conclusions.

comment:15 Changed 3 years ago by bgamari

I also say that your Fun is quite wrong. I prefer this one:

That is true and I implement your variant in the branch; I probably should have written Fun as a GADT-style constructor of TypeRep to avoid confusion.

comment:16 Changed 3 years ago by simonpj

But do we need the full glory of typeRepKind, or just the ability to look at (->) levity arguments?

comment:17 Changed 3 years ago by simonpj

Keywords: LevityPolymorphism added

comment:18 Changed 3 years ago by bgamari

@simonpj, I believe we need typeRepKind. However, I'm well on my way to implementing it. Unfortunately I'm somewhat blocked on #12905.

comment:19 Changed 3 years ago by bgamari

Owner: set to goldfire
Priority: normalhigh

Richard should be taking care of this as part of the levity polymorphism work.

comment:20 Changed 3 years ago by bgamari

Resolution: fixed
Status: newclosed

This is now fixed.

comment:21 Changed 22 months ago by simonpj

Keywords: Typeable added; typeable removed
Note: See TracTickets for help on using tickets.