Fix #11473.
authorRichard Eisenberg <eir@cis.upenn.edu>
Tue, 15 Mar 2016 18:27:22 +0000 (14:27 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 16 Mar 2016 01:19:20 +0000 (21:19 -0400)
I've added a check in the zonker for representation polymorphism.
I don't like having this be in the zonker, but I don't know where
else to put it. It can't go in TcValidity, because a clever enough
user could convince the solver to do bogus representation polymorphism
even though there's nothing obviously wrong in what they wrote.
Note that TcValidity doesn't run over *expressions*, which is where
this problem arises.

In any case, the check is simple and it works.

test case: dependent/should_fail/T11473

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

index 6e35a2b..c1609c0 100644 (file)
@@ -279,6 +279,7 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids
 zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
 zonkIdBndr env id
   = do ty' <- zonkTcTypeToType env (idType id)
+       ensureNotRepresentationPolymorphic id ty'
        return (setIdType id ty')
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
@@ -459,19 +460,34 @@ zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
                         , abe_mono = zonkIdOcc env mono_id
                         , abe_prags = new_prags })
 
-zonk_bind env (AbsBindsSig { abs_tvs         = tyvars
-                           , abs_ev_vars     = evs
-                           , abs_sig_export  = poly
-                           , abs_sig_prags   = prags
-                           , abs_sig_ev_bind = ev_bind
-                           , abs_sig_bind    = bind })
+zonk_bind env outer_bind@(AbsBindsSig { abs_tvs         = tyvars
+                                      , abs_ev_vars     = evs
+                                      , abs_sig_export  = poly
+                                      , abs_sig_prags   = prags
+                                      , abs_sig_ev_bind = ev_bind
+                                      , abs_sig_bind    = lbind })
+  | L bind_loc bind@(FunBind { fun_id      = L loc local
+                             , fun_matches = ms
+                             , fun_co_fn   = co_fn }) <- lbind
   = ASSERT( all isImmutableTyVar tyvars )
     do { (env0, new_tyvars)  <- zonkTyBndrsX env  tyvars
        ; (env1, new_evs)     <- zonkEvBndrsX env0 evs
        ; (env2, new_ev_bind) <- zonkTcEvBinds env1 ev_bind
-       ; new_val_bind        <- zonk_lbind env2 bind
+           -- Inline zonk_bind (FunBind ...) because we wish to skip
+           -- the check for representation-polymorphic binders. The
+           -- local binder in the FunBind in an AbsBindsSig is never actually
+           -- bound in Core -- indeed, that's the whole point of AbsBindsSig.
+           -- just calling zonk_bind causes #11405.
+       ; new_local           <- updateVarTypeM (zonkTcTypeToType env2) local
+       ; (env3, new_co_fn)   <- zonkCoFn env2 co_fn
+       ; new_ms              <- zonkMatchGroup env3 zonkLExpr ms
+           -- If there is a representation polymorphism problem, it will
+           -- be caught here:
        ; new_poly_id         <- zonkIdBndr env2 poly
        ; new_prags           <- zonkSpecPrags env2 prags
+       ; let new_val_bind = L bind_loc (bind { fun_id      = L loc new_local
+                                             , fun_matches = new_ms
+                                             , fun_co_fn   = new_co_fn })
        ; return (AbsBindsSig { abs_tvs         = new_tyvars
                              , abs_ev_vars     = new_evs
                              , abs_sig_export  = new_poly_id
@@ -479,6 +495,9 @@ zonk_bind env (AbsBindsSig { abs_tvs         = tyvars
                              , abs_sig_ev_bind = new_ev_bind
                              , abs_sig_bind    = new_val_bind  }) }
 
+  | otherwise
+  = pprPanic "zonk_bind" (ppr outer_bind)
+
 zonk_bind env (PatSynBind bind@(PSB { psb_id = L loc id
                                     , psb_args = details
                                     , psb_def = lpat
@@ -1628,3 +1647,34 @@ zonkTypeZapping tv
                 | otherwise          = anyTypeOfKind (tyVarKind tv)
        ; writeMetaTyVar tv ty
        ; return ty }
+
+---------------------------------------
+-- | 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
+-- that we respect this rule. It is a bit regrettable that this error
+-- occurs in zonking, after which we should have reported all errors.
+-- But it's hard to see where else to do it, because this can be discovered
+-- only after all solving is done. And, perhaps most importantly, this
+-- 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
+  -> TcM ()
+ensureNotRepresentationPolymorphic id ty
+  = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
+                   -- forall a. a. See, for example, test ghci/scripts/T9140
+    unless (isEmptyVarSet (tyCoVarsOfType ki)) $
+    addErrAt (nameSrcSpan $ idName id) $
+    vcat [ text "The following variable has an unknown runtime representation:"
+         , text "    Var name:" <+> ppr id
+         , text "    Var type:" <+> ppr tidy_ty
+         , text " Type's kind:" <+> ppr tidy_ki
+         , text "Perhaps add a type or kind signature to fix the representation."
+         ]
+  where
+    ki = typeKind ty
+
+    (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
+    tidy_ki             = tidyType tidy_env ki
diff --git a/testsuite/tests/dependent/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs
new file mode 100644 (file)
index 0000000..12d95ca
--- /dev/null
@@ -0,0 +1,27 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
+
+module T11473 where
+
+import GHC.Exts
+import GHC.Types
+
+type family Boxed (a :: k) :: *
+type instance Boxed Char# = Char
+type instance Boxed Char  = Char
+
+class BoxIt (a :: TYPE lev) where
+    boxed :: a -> Boxed a
+
+instance BoxIt Char# where boxed x = C# x
+instance BoxIt Char  where boxed = id
+
+hello :: forall (r :: RuntimeRep). forall (a :: TYPE r). BoxIt a => a -> Boxed a
+hello x = boxed x
+{-# NOINLINE hello #-}
+
+main :: IO ()
+main = do
+    print $ boxed 'c'#
+    print $ boxed 'c'
+    print $ hello 'c'
+    print $ hello 'c'#
diff --git a/testsuite/tests/dependent/should_fail/T11473.stderr b/testsuite/tests/dependent/should_fail/T11473.stderr
new file mode 100644 (file)
index 0000000..7a7cc32
--- /dev/null
@@ -0,0 +1,7 @@
+
+T11473.hs:19:7: error:
+    The following variable has an unknown runtime representation:
+        Var name: x
+        Var type: a
+     Type's kind: TYPE r
+    Perhaps add a type or kind signature to fix the representation.
index a90b7bb..c75a9c6 100644 (file)
@@ -12,3 +12,4 @@ test('T11407', normal, compile_fail, [''])
 test('T11334', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
 test('KindLevelsB', normal, compile_fail, [''])
+test('T11473', normal, compile_fail, [''])