Fix #11512 by getting visibility right for methods

Test case: typecheck/should_compile/T11512

compiler/basicTypes/MkId.hs

@@ -262,9 +262,6 @@ Then the top-level type for op is
               forall b. Ord b =>
               a -> b -> b
 
-This is unlike ordinary record selectors, which have all the for-alls
-at the outside.  When dealing with classes it's very convenient to
-recover the original type signature from the class op selector.
 -}
 
 mkDictSelId :: Name          -- Name of one of the *value* selectors
@@ -278,11 +275,23 @@ mkDictSelId name clas
     new_tycon      = isNewTyCon tycon
     [data_con]     = tyConDataCons tycon
     tyvars         = dataConUnivTyVars data_con
+    tc_binders     = tyConBinders tycon
     arg_tys        = dataConRepArgTys data_con  -- Includes the dictionary superclasses
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
 
-    sel_ty = mkSpecForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars))
-                                             (getNth arg_tys val_index))
+    sel_ty = mkForAllTys (zipWith mk_binder tc_binders tyvars) $
+             mkFunTy (mkClassPred clas (mkTyVarTys tyvars)) $
+             getNth arg_tys val_index
+
+      -- copy the visibility from the tycon binders. Consider:
+      --   class C a where foo :: Proxy a
+      -- In the type of foo, `a` must be Specified but `k` must be Invisible
+    mk_binder tc_binder tyvar
+      | Invisible <- binderVisibility tc_binder
+      = mkNamedBinder Invisible tyvar
+      | otherwise
+      = mkNamedBinder Specified tyvar   -- don't just copy from tc_binder, because
+                                        -- tc_binders can be Visible
 
     base_info = noCafIdInfo
                 `setArityInfo`         1

compiler/typecheck/TcExpr.hs

@@ -1175,7 +1175,10 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
            ; case tcSplitForAllTy_maybe upsilon_ty of
                Just (binder, inner_ty)
                  | Just tv <- binderVar_maybe binder ->
-                 ASSERT( binderVisibility binder == Specified )
+                 ASSERT2( binderVisibility binder == Specified
+                        , (vcat [ ppr fun_ty, ppr upsilon_ty, ppr binder
+                                , ppr inner_ty, pprTvBndr tv
+                                , ppr (binderVisibility binder) ]) )
                  do { let kind = tyVarKind tv
                     ; ty_arg <- tcHsTypeApp hs_ty_arg kind
                     ; let insted_ty = substTyWithUnchecked [tv] [ty_arg] inner_ty

testsuite/tests/dependent/should_compile/RaeJobTalk.hs

@@ -217,7 +217,7 @@ instance TyConAble RuntimeRep    where tyCon = RuntimeRep
 
 -- Can't just define Typeable the way we want, because the instances
 -- overlap. So we have to mock up instance chains via closed type families.
-class Typeable' (a :: k) (b :: Bool) where
+class Typeable' a (b :: Bool) where
   typeRep' :: TypeRep a
 
 type family CheckPrim a where
@@ -236,7 +236,7 @@ instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
   typeRep' = TyApp typeRep typeRep
 
 typeRep :: forall a. Typeable a => TypeRep a
-typeRep = typeRep' @_ @_ @(CheckPrim a) -- RAE: #11512 says we need the extra @_.
+typeRep = typeRep' @_ @(CheckPrim a)
 
 -----------------------------
 -- Useful instances

testsuite/tests/typecheck/should_compile/T11512.hs

+{-# LANGUAGE PolyKinds, TypeApplications, ScopedTypeVariables #-}
+
+module Bug where
+
+import Data.Proxy
+
+class C a where
+  foo :: Proxy a
+
+bar :: forall a. C a => Proxy a
+bar = foo @a

testsuite/tests/typecheck/should_compile/all.T

@@ -509,3 +509,4 @@ test('T11246', normal, compile, [''])
 test('T11608', normal, compile, [''])
 test('T11401', normal, compile, [''])
 test('T11699', normal, compile, [''])
+test('T11512', normal, compile, [''])