Check for rep poly on wildcard binders.
authorRichard Eisenberg <eir@cis.upenn.edu>
Fri, 25 Mar 2016 20:18:09 +0000 (16:18 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Sat, 26 Mar 2016 20:28:27 +0000 (16:28 -0400)
I had just missed this case when adding my test.
This is relevant to ticket #11473.

Also adds lots of comments.

compiler/typecheck/TcHsSyn.hs
testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 88110b7..f6fa01a 100644 (file)
@@ -283,7 +283,8 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids
 zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
 zonkIdBndr env id
   = do ty' <- zonkTcTypeToType env (idType id)
-       ensureNotRepresentationPolymorphic id ty'
+       ensureNotRepresentationPolymorphic ty'
+         (text "In the type of binder" <+> quotes (ppr id))
        return (setIdType id ty')
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
@@ -1160,6 +1161,8 @@ zonk_pat env (ParPat p)
 
 zonk_pat env (WildPat ty)
   = do  { ty' <- zonkTcTypeToType env ty
+        ; ensureNotRepresentationPolymorphic ty'
+            (text "In a wildcard pattern")
         ; return (env, WildPat ty') }
 
 zonk_pat env (VarPat (L l v))
@@ -1653,6 +1656,70 @@ zonkTypeZapping tv
        ; return ty }
 
 ---------------------------------------
+{-
+Note [Unboxed tuples in representation polymorphism check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Recall that all types that have values (that is, lifted and unlifted
+types) have kinds that look like (TYPE rep), where (rep :: RuntimeRep)
+tells how the values are represented at runtime. Lifted types have
+kind (TYPE PtrRepLifted) (for which * is just a synonym) and, say,
+Int# has kind (TYPE IntRep).
+
+It would be terrible if the code generator came upon a binder of a type
+whose kind is something like TYPE r, where r is a skolem type variable.
+The code generator wouldn't know what to do. So we eliminate that case
+here.
+
+Although representation polymorphism and the RuntimeRep type catch
+most ways of abusing unlifted types, it still isn't quite satisfactory
+around unboxed tuples. That's because all unboxed tuple types have kind
+TYPE UnboxedTupleRep, which is clearly a lie: it doesn't actually tell
+you what the representation is.
+
+Naively, when checking for representation polymorphism, you might think we can
+just look for free variables in a type's RuntimeRep. But this misses the
+UnboxedTupleRep case.
+
+So, instead, we handle unboxed tuples specially. Only after unboxed tuples
+are handled do we look for free tyvars in a RuntimeRep.
+
+We must still be careful in the UnboxedTupleRep case. A binder whose type
+has kind UnboxedTupleRep is OK -- only as long as the type is really an
+unboxed tuple, which the code generator treats specially. So we do this:
+ 1. Check if the type is an unboxed tuple. If so, recur.
+ 2. Check if the kind is TYPE UnboxedTupleRep. If so, error.
+ 3. Check if the kind has any free variables. If so, error.
+
+In case 1, we have a type that looks like
+
+  (# , #) PtrRepLifted IntRep Bool Int#
+
+recalling that
+
+  (# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep).
+             TYPE r1 -> TYPE r2 -> TYPE UnboxedTupleRep
+
+It's tempting just to look at the RuntimeRep arguments to make sure
+that they are devoid of free variables and not UnboxedTupleRep. This
+naive check, though, fails on nested unboxed tuples, like
+(# Int#, (# Bool, Void# #) #). Thus, instead of looking at the RuntimeRep
+args to the unboxed tuple constructor, we look at the types themselves.
+
+Here are a few examples:
+
+   type family F r :: TYPE r
+
+   x :: (F r :: TYPE r)   -- REJECTED: simple representation polymorphism
+     where r is an in-scope type variable of kind RuntimeRep
+
+   x :: (F PtrRepLifted :: TYPE PtrRepLifted)   -- OK
+   x :: (F IntRep       :: TYPE IntRep)         -- OK
+
+   x :: (F UnboxedTupleRep :: TYPE UnboxedTupleRep)  -- REJECTED
+
+   x :: ((# Int, Bool #) :: TYPE UnboxedTupleRep)    -- OK
+-}
+
 -- | According to the rules around representation polymorphism
 -- (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder
 -- can have a representation-polymorphic type. This check ensures
@@ -1663,24 +1730,20 @@ zonkTypeZapping tv
 -- isn't really a compositional property of a type system, so it's
 -- not a terrible surprise that the check has to go in an awkward spot.
 ensureNotRepresentationPolymorphic
-  :: TcId  -- the id we're checking (for errors only)
-  -> Type  -- its zonked type
+  :: Type  -- its zonked type
+  -> SDoc  -- where this happened
   -> TcM ()
-ensureNotRepresentationPolymorphic id ty
+ensureNotRepresentationPolymorphic ty doc
   = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
                    -- forall a. a. See, for example, test ghci/scripts/T9140
-    checkForRepresentationPolymorphism
-      (text "In the type of binder" <+> quotes (ppr id)) ty
+    checkForRepresentationPolymorphism doc ty
 
+   -- See Note [Unboxed tuples in representation polymorphism check]
 checkForRepresentationPolymorphism :: SDoc -> Type -> TcM ()
 checkForRepresentationPolymorphism extra ty
   | Just (tc, tys) <- splitTyConApp_maybe ty
   , isUnboxedTupleTyCon tc
   = mapM_ (checkForRepresentationPolymorphism extra) (dropRuntimeRepArgs tys)
-      -- You might think that we can just check the RuntimeRep args themselves.
-      -- But this would fail in the case of nested unboxed tuples, for which
-      -- one of the RuntimeRep args would be UnboxedTupleRep. So we just check
-      -- the type args directly.
 
   | runtime_rep `eqType` unboxedTupleRepDataConTy
   = addErr (vcat [ text "The type" <+> quotes (ppr tidy_ty) <+>
diff --git a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs b/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs
new file mode 100644 (file)
index 0000000..2935416
--- /dev/null
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, KindSignatures, TypeInType #-}
+
+module BadUnboxedTuple where
+
+import GHC.Exts
+
+type family F :: TYPE UnboxedTupleRep
+
+foo :: F -> ()
+foo _ = ()
diff --git a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr b/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr
new file mode 100644 (file)
index 0000000..7c5ad57
--- /dev/null
@@ -0,0 +1,6 @@
+
+BadUnboxedTuple.hs:10:5: error:
+    The type â€˜F’ is not an unboxed tuple,
+    and yet its kind suggests that it has the representation
+    of an unboxed tuple. This is not allowed.
+    In a wildcard pattern
index f24736e..867ea38 100644 (file)
@@ -411,3 +411,4 @@ test('T11541', normal, compile_fail, [''])
 test('T11313', normal, compile_fail, [''])
 test('T11723', normal, compile_fail, [''])
 test('T11724', normal, compile_fail, [''])
+test('BadUnboxedTuple', normal, compile_fail, [''])