Fix #15637 by using VTA more in GND
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 1 Oct 2018 16:00:52 +0000 (12:00 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Mon, 1 Oct 2018 16:00:53 +0000 (12:00 -0400)
Summary:
The code that GND was generating before could crumple over
if it derived an instance for a class with an ambiguous type variable
in the class head, such as the example in #15637. The solution is
straightforward: simply instantiate all variables bound by the class
head explicitly using visible type application, which will nip any
ambiguity in the bud.

Test Plan: make test TEST=T15637

Reviewers: bgamari, simonpj, goldfire

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, carter

GHC Trac Issues: #15637

Differential Revision: https://phabricator.haskell.org/D5148

compiler/typecheck/FamInst.hs
compiler/typecheck/TcGenDeriv.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs
compiler/types/Type.hs
testsuite/tests/deriving/should_compile/T14578.stderr
testsuite/tests/deriving/should_compile/T15637.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/all.T
testsuite/tests/deriving/should_fail/T15073.stderr
testsuite/tests/deriving/should_fail/T4846.stderr

index 00602ec..dc6eab8 100644 (file)
@@ -763,11 +763,15 @@ unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
 unusedInjTvsInRHS tycon injList lhs rhs =
   (`minusVarSet` injRhsVars) <$> injLHSVars
     where
+      inj_pairs :: [(Type, ArgFlag)]
+      -- All the injective arguments, paired with their visiblity
+      inj_pairs = ASSERT2( injList `equalLength` lhs
+                         , ppr tycon $$ ppr injList $$ ppr lhs )
+                  filterByList injList (lhs `zip` tyConArgFlags tycon lhs)
+
       -- set of type and kind variables in which type family is injective
-      (invis_pairs, vis_pairs)
-        = partitionInvisibles tycon snd (zipEqual "unusedInjTvsInRHS" injList lhs)
-      invis_lhs = uncurry filterByList $ unzip invis_pairs
-      vis_lhs   = uncurry filterByList $ unzip vis_pairs
+      invis_lhs, vis_lhs :: [Type]
+      (invis_lhs, vis_lhs) = partitionInvisibles inj_pairs
 
       invis_vars = tyCoVarsOfTypes invis_lhs
       Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
index 1debddd..32f081b 100644 (file)
@@ -1746,6 +1746,33 @@ a truly higher-rank type like so:
 
 Then the same situation will arise again. But at least it won't arise for the
 common case of methods with ordinary, prenex-quantified types.
+
+Note [GND and ambiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We make an effort to make the code generated through GND be robust w.r.t.
+ambiguous type variables. As one example, consider the following example
+(from #15637):
+
+  class C a where f :: String
+  instance C () where f = "foo"
+  newtype T = T () deriving C
+
+A naïve attempt and generating a C T instance would be:
+
+  instance C T where
+    f = coerce @String @String f
+          :: String
+
+This isn't going to typecheck, however, since GHC doesn't know what to
+instantiate the type variable `a` with in the call to `f` in the method body.
+(Note that `f :: forall a. String`!) To compensate for the possibility of
+ambiguity here, we explicitly instantiate `a` like so:
+
+  instance C T where
+    f = coerce @String @String (f @())
+          :: String
+
+All better now.
 -}
 
 gen_Newtype_binds :: SrcSpan
@@ -1779,9 +1806,17 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         rhs_expr = nlHsVar (getRdrName coerceId)
                                       `nlHsAppType`     from_tau
                                       `nlHsAppType`     to_tau
-                                      `nlHsApp`         nlHsVar meth_RDR
+                                      `nlHsApp`         meth_app
                                       `nlExprWithTySig` to_ty
 
+        -- The class method, applied to all of the class instance types
+        -- (including the representation type) to avoid potential ambiguity.
+        -- See Note [GND and ambiguity]
+        meth_app = foldl' nlHsAppType (nlHsVar meth_RDR) $
+                   filterOutInferredTypes (classTyCon cls) underlying_inst_tys
+                     -- Filter out any inferred arguments, since they can't be
+                     -- applied with visible type application.
+
     mk_atf_inst :: TyCon -> TcM FamInst
     mk_atf_inst fam_tc = do
         rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc))
@@ -1797,7 +1832,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         in_scope    = mkInScopeSet $ mkVarSet inst_tvs
         lhs_env     = zipTyEnv cls_tvs inst_tys
         lhs_subst   = mkTvSubst in_scope lhs_env
-        rhs_env     = zipTyEnv cls_tvs $ changeLast inst_tys rhs_ty
+        rhs_env     = zipTyEnv cls_tvs underlying_inst_tys
         rhs_subst   = mkTvSubst in_scope rhs_env
         fam_tvs     = tyConTyVars fam_tc
         rep_lhs_tys = substTyVars lhs_subst fam_tvs
@@ -1809,6 +1844,11 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         rep_cvs'    = toposortTyVars rep_cvs
         pp_lhs      = ppr (mkTyConApp fam_tc rep_lhs_tys)
 
+    -- Same as inst_tys, but with the last argument type replaced by the
+    -- representation type.
+    underlying_inst_tys :: [Type]
+    underlying_inst_tys = changeLast inst_tys rhs_ty
+
 nlHsAppType :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
 nlHsAppType e s = noLoc (HsAppType hs_ty e)
   where
@@ -1831,7 +1871,7 @@ mkCoerceClassMethEqn :: Class   -- the class being derived
 -- See Note [Newtype-deriving instances]
 -- See also Note [Newtype-deriving trickiness]
 -- The pair is the (from_type, to_type), where to_type is
--- the type of the method we are tyrying to get
+-- the type of the method we are trying to get
 mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty id
   = Pair (substTy rhs_subst user_meth_ty)
          (substTy lhs_subst user_meth_ty)
index eafb5b3..8419b90 100644 (file)
@@ -3305,13 +3305,16 @@ checkValidRoleAnnots role_annots tc
     -- but a tycon stores roles for all variables.
     -- So, we drop the implicit roles (which are all Nominal, anyway).
     name                   = tyConName tc
-    tyvars                 = tyConTyVars tc
     roles                  = tyConRoles tc
-    (vis_roles, vis_vars)  = unzip $ snd $
-                             partitionInvisibles tc (mkTyVarTy . snd) $
-                             zip roles tyvars
+    (vis_roles, vis_vars)  = unzip $ mapMaybe pick_vis $
+                             zip roles (tyConBinders tc)
     role_annot_decl_maybe  = lookupRoleAnnot role_annots name
 
+    pick_vis :: (Role, TyConBinder) -> Maybe (Role, TyVar)
+    pick_vis (role, tvb)
+      | isVisibleTyConBinder tvb = Just (role, binderVar tvb)
+      | otherwise                = Nothing
+
     check_roles
       = whenIsJust role_annot_decl_maybe $
           \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) ->
index dab9f2c..12f1ac7 100644 (file)
@@ -1766,7 +1766,9 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
     arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
                  | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
 
-    (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes
+    kind_shapes, type_shapes :: [AssocInstArgShape]
+    (kind_shapes, type_shapes) = partitionInvisibles $
+                                 arg_shapes `zip` tyConArgFlags fam_tc at_tys
 
     check_arg :: AssocInstArgShape -> Bool
     check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
index bda3602..9012815 100644 (file)
@@ -62,8 +62,8 @@ module Type (
         coAxNthLHS,
         stripCoercionTy, splitCoercionType_maybe,
 
-        splitPiTysInvisible, filterOutInvisibleTypes,
-        partitionInvisibleTypes, partitionInvisibles,
+        splitPiTysInvisible, filterOutInvisibleTypes, filterOutInferredTypes,
+        partitionInvisibleTypes, partitionInvisibles, tyConArgFlags,
         synTyConResKind,
 
         modifyJoinResTy, setJoinResTy,
@@ -262,7 +262,6 @@ import Unique ( nonDetCmpUnique )
 import Maybes           ( orElse )
 import Data.Maybe       ( isJust, mapMaybe )
 import Control.Monad    ( guard )
-import Control.Arrow    ( first, second )
 
 -- $type_classification
 -- #type_classification#
@@ -1544,23 +1543,43 @@ splitPiTysInvisible ty = split ty ty []
       | isPredTy arg                   = split res res (Anon arg : bs)
     split orig_ty _                bs  = (reverse bs, orig_ty)
 
--- | Given a tycon and its arguments, filters out any invisible arguments
+-- | Given a 'TyCon' and a list of argument types, filter out any invisible
+-- (i.e., 'Inferred' or 'Specified') arguments.
 filterOutInvisibleTypes :: TyCon -> [Type] -> [Type]
 filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys
 
--- | Given a 'TyCon' and its arguments, partition the arguments into
--- (invisible arguments, visible arguments).
+-- | Given a 'TyCon' and a list of argument types, filter out any 'Inferred'
+-- arguments.
+filterOutInferredTypes :: TyCon -> [Type] -> [Type]
+filterOutInferredTypes tc tys =
+  filterByList (map (/= Inferred) $ tyConArgFlags tc tys) tys
+
+-- | Given a 'TyCon' and a list of argument types, partition the arguments
+-- into:
+--
+-- 1. 'Inferred' or 'Specified' (i.e., invisible) arguments and
+--
+-- 2. 'Required' (i.e., visible) arguments
 partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type])
-partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
+partitionInvisibleTypes tc tys =
+  partitionByList (map isInvisibleArgFlag $ tyConArgFlags tc tys) tys
 
--- | Given a tycon and a list of things (which correspond to arguments),
--- partitions the things into
---      Inferred or Specified ones and
---      Required ones
--- The callback function is necessary for this scenario:
+-- | Given a list of things paired with their visibilities, partition the
+-- things into (invisible things, visible things).
+partitionInvisibles :: [(a, ArgFlag)] -> ([a], [a])
+partitionInvisibles = partitionWith pick_invis
+  where
+    pick_invis :: (a, ArgFlag) -> Either a a
+    pick_invis (thing, vis) | isInvisibleArgFlag vis = Left thing
+                            | otherwise              = Right thing
+
+-- | Given a 'TyCon' and a list of argument types, determine each argument's
+-- visibility ('Inferred', 'Specified', or 'Required').
+--
+-- Wrinkle: consider the following scenario:
 --
 -- > T :: forall k. k -> k
--- > partitionInvisibles T [forall m. m -> m -> m, S, R, Q]
+-- > tyConArgFlags T [forall m. m -> m -> m, S, R, Q]
 --
 -- After substituting, we get
 --
@@ -1568,23 +1587,19 @@ partitionInvisibleTypes tc tys = partitionInvisibles tc id tys
 --
 -- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again,
 -- and @Q@ is visible.
---
--- If you're absolutely sure that your tycon's kind doesn't end in a variable,
--- it's OK if the callback function panics, as that's the only time it's
--- consulted.
-partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
-partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
+tyConArgFlags :: TyCon -> [Type] -> [ArgFlag]
+tyConArgFlags tc = go emptyTCvSubst (tyConKind tc)
   where
-    go _ _ [] = ([], [])
-    go subst (ForAllTy (Bndr tv vis) res_ki) (x:xs)
-      | isVisibleArgFlag vis = second (x :) (go subst' res_ki xs)
-      | otherwise            = first  (x :) (go subst' res_ki xs)
+    go _ _ [] = []
+    go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys)
+      = argf : go subst' res_ki arg_tys
       where
-        subst' = extendTCvSubst subst tv (get_ty x)
-    go subst (TyVarTy tv) xs
-      | Just ki <- lookupTyVar subst tv = go subst ki xs
-    go _ _ xs = ([], xs)  -- something is ill-kinded. But this can happen
-                          -- when printing errors. Assume everything is visible.
+        subst' = extendTvSubst subst tv arg_ty
+    go subst (TyVarTy tv) arg_tys
+      | Just ki <- lookupTyVar subst tv = go subst ki arg_tys
+    go _ _ arg_tys = map (const Required) arg_tys
+                        -- something is ill-kinded. But this can happen
+                        -- when printing errors. Assume everything is Required.
 
 -- @isTauTy@ tests if a type has no foralls
 isTauTy :: Type -> Bool
@@ -2832,7 +2847,7 @@ splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
 
     invisible vs = Pair vs emptyVarSet
 
-    go_tc tc tys = let (invis, vis) = partitionInvisibles tc id tys in
+    go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in
                    invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis
 
 splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet
index 9f7ef67..78861f6 100644 (file)
@@ -7,7 +7,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @((a -> b) -> f a -> f b)
           @((a -> b) -> T14578.App f a -> T14578.App f b)
-          GHC.Base.fmap ::
+          (GHC.Base.fmap @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep).
           (a -> b) -> T14578.App f a -> T14578.App f b
@@ -15,7 +15,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(a -> f b -> f a)
           @(a -> T14578.App f b -> T14578.App f a)
-          (GHC.Base.<$) ::
+          ((GHC.Base.<$) @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep).
           a -> T14578.App f b -> T14578.App f a
@@ -24,13 +24,13 @@ Derived class instances:
            GHC.Base.Applicative (T14578.App f) where
     GHC.Base.pure
       = GHC.Prim.coerce
-          @(a -> f a) @(a -> T14578.App f a) GHC.Base.pure ::
+          @(a -> f a) @(a -> T14578.App f a) (GHC.Base.pure @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep). a -> T14578.App f a
     (GHC.Base.<*>)
       = GHC.Prim.coerce
           @(f (a -> b) -> f a -> f b)
           @(T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b)
-          (GHC.Base.<*>) ::
+          ((GHC.Base.<*>) @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep).
           T14578.App f (a -> b) -> T14578.App f a -> T14578.App f b
@@ -39,7 +39,7 @@ Derived class instances:
           @((a -> b -> c) -> f a -> f b -> f c)
           @((a -> b -> c)
             -> T14578.App f a -> T14578.App f b -> T14578.App f c)
-          GHC.Base.liftA2 ::
+          (GHC.Base.liftA2 @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep)
                  (c :: TYPE GHC.Types.LiftedRep).
@@ -48,7 +48,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(f a -> f b -> f b)
           @(T14578.App f a -> T14578.App f b -> T14578.App f b)
-          (GHC.Base.*>) ::
+          ((GHC.Base.*>) @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep).
           T14578.App f a -> T14578.App f b -> T14578.App f b
@@ -56,7 +56,7 @@ Derived class instances:
       = GHC.Prim.coerce
           @(f a -> f b -> f a)
           @(T14578.App f a -> T14578.App f b -> T14578.App f a)
-          (GHC.Base.<*) ::
+          ((GHC.Base.<*) @f) ::
           forall (a :: TYPE GHC.Types.LiftedRep)
                  (b :: TYPE GHC.Types.LiftedRep).
           T14578.App f a -> T14578.App f b -> T14578.App f a
@@ -73,7 +73,9 @@ Derived class instances:
                -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                   -> TYPE GHC.Types.LiftedRep) a)
           @(T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a)
-          (GHC.Base.<>) ::
+          ((GHC.Base.<>)
+             @(T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
+                                                               -> TYPE GHC.Types.LiftedRep) a)) ::
           T14578.Wat f g a -> T14578.Wat f g a -> T14578.Wat f g a
     GHC.Base.sconcat
       = GHC.Prim.coerce
@@ -82,7 +84,9 @@ Derived class instances:
             -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                -> TYPE GHC.Types.LiftedRep) a)
           @(GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a)
-          GHC.Base.sconcat ::
+          (GHC.Base.sconcat
+             @(T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
+                                                               -> TYPE GHC.Types.LiftedRep) a)) ::
           GHC.Base.NonEmpty (T14578.Wat f g a) -> T14578.Wat f g a
     GHC.Base.stimes
       = GHC.Prim.coerce
@@ -92,7 +96,9 @@ Derived class instances:
                -> T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
                                                                   -> TYPE GHC.Types.LiftedRep) a)
           @(b -> T14578.Wat f g a -> T14578.Wat f g a)
-          GHC.Base.stimes ::
+          (GHC.Base.stimes
+             @(T14578.App (Data.Functor.Compose.Compose f g :: TYPE GHC.Types.LiftedRep
+                                                               -> TYPE GHC.Types.LiftedRep) a)) ::
           forall (b :: TYPE GHC.Types.LiftedRep).
           GHC.Real.Integral b => b -> T14578.Wat f g a -> T14578.Wat f g a
   
diff --git a/testsuite/tests/deriving/should_compile/T15637.hs b/testsuite/tests/deriving/should_compile/T15637.hs
new file mode 100644 (file)
index 0000000..26bfe07
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GeneralisedNewtypeDeriving #-}
+module T15637 where
+
+class C a where f :: String
+
+instance C () where f = "foo"
+
+newtype T = T () deriving C
index cc0730f..c49b808 100644 (file)
@@ -112,3 +112,4 @@ test('T14933', normal, compile, [''])
 test('T15290c', normal, compile, [''])
 test('T15290d', normal, compile, [''])
 test('T15398', normal, compile, [''])
+test('T15637', normal, compile, [''])
index 87fd7e5..2cc3f90 100644 (file)
@@ -11,7 +11,7 @@ T15073.hs:8:12: error:
               -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
             @(Foo a
               -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-            p ::
+            (p @a) ::
             Foo a
             -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
       In an equation for ‘p’:
@@ -20,7 +20,7 @@ T15073.hs:8:12: error:
                   -> (Unit# a :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
                 @(Foo a
                   -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep))))
-                p ::
+                (p @a) ::
                 Foo a
                 -> (Unit# (Foo a) :: TYPE (GHC.Types.TupleRep ((:) GHC.Types.LiftedRep ([] :: [] GHC.Types.RuntimeRep) :: [] GHC.Types.RuntimeRep)))
       When typechecking the code for ‘p’
index 428f1a5..9fe54c6 100644 (file)
@@ -3,10 +3,12 @@ T4846.hs:29:1: error:
     • Couldn't match type ‘Bool’ with ‘BOOL’
         arising from a use of ‘GHC.Prim.coerce’
     • In the expression:
-          GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr :: Expr BOOL
+          GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) (mkExpr @Bool) ::
+            Expr BOOL
       In an equation for ‘mkExpr’:
           mkExpr
-            = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr :: Expr BOOL
+            = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) (mkExpr @Bool) ::
+                Expr BOOL
       When typechecking the code for ‘mkExpr’
         in a derived instance for ‘B BOOL’:
         To see the code I am typechecking, use -ddump-deriv