#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 representationpolymorphic 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:2 Changed 3 years ago by
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 wellkinded 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
comment:3 Changed 3 years ago by
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) :: *)’ Illkinded 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:5 Changed 3 years ago by
Simonpj, which fix is this? I haven't seen a fix for #12668 yet; presumably it has yet to be merged?
comment:7 Changed 3 years ago by
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 13 13 ) where 14 14 15 15 import HsSyn 16 import TcHsSyn( checkForRepresentationPolymorphism ) 16 17 import TcPat 17 18 import Type( mkTyVarBinders, mkEmptyTCvSubst 18 19 , tidyTyVarBinders, tidyTypes, tidyType ) … … tc_patsyn_finish lname dir is_infix lpat' 312 313 arg_tys = tidyTypes env2 arg_tys' 313 314 pat_ty = tidyType env2 pat_ty' 314 315 316  Check that the arguments aren't representationally polymorphic 317 ; mapM_ (checkForRepresentationPolymorphism empty) arg_tys 318 315 319 ; traceTc "tc_patsyn_finish {" $ 316 320 ppr (unLoc lname) $$ ppr (unLoc lpat') $$ 317 321 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 2296 2296  Check all argument types for validity 2297 2297 ; checkValidType ctxt (dataConUserType con) 2298 2298 2299  Check for representationally polymorphic fields 2300 ; mapM_ (checkForRepresentationPolymorphism empty) (dataConOrigArgTys con) 2301 2299 2302  Extra checks for newtype data constructors 2300 2303 ; when (isNewTyCon tc) (checkNewDataCon con) 2301 2304 
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 () 487 487 488 488 check_type env ctxt rank (FunTy arg_ty res_ty) 489 489 = do { check_type env ctxt arg_rank arg_ty 490 ; when (representationPolymorphismForbidden ctxt) $491 checkForRepresentationPolymorphism empty arg_ty492 490 ; check_type env ctxt res_rank res_ty } 493 491 where 494 492 (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
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
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, revalidate, etc). Soon. Soon.
comment:10 Changed 3 years ago by
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.
comment:11 Changed 3 years ago by
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
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 polykinded.   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))
In sum, if we allow arrow to be polymorphic in its result type's kind, then we need typeRepKind
to safely apply Dynamic
values, since we the applied function may produce a nonlifted result.
comment:13 followup: 14 Changed 3 years ago by
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 Changed 3 years ago by
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
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 GADTstyle constructor of TypeRep
to avoid confusion.
comment:16 Changed 3 years ago by
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
Keywords:  LevityPolymorphism added 

comment:18 Changed 3 years ago by
@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
Owner:  set to goldfire 

Priority:  normal → high 
Richard should be taking care of this as part of the levity polymorphism work.
comment:21 Changed 21 months ago by
Keywords:  Typeable added; typeable removed 

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