Refactor handling of decomposition.
authorRichard Eisenberg <eir@cis.upenn.edu>
Mon, 15 Jun 2015 21:02:36 +0000 (17:02 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Tue, 16 Jun 2015 18:22:52 +0000 (14:22 -0400)
This adds the significant Note [Decomposing equalities] to
TcCanonical, trying to sort out the various cases involved.

The only functional change this commit should make is a different
treatment of data families, which were wrong before (they could
be decomposed at role R, which is wrong).

compiler/coreSyn/CoreLint.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcUnify.hs
compiler/types/Coercion.hs
compiler/types/OptCoercion.hs
compiler/types/TyCon.hs
compiler/types/Type.hs
testsuite/tests/typecheck/should_compile/RepArrow.hs [new file with mode: 0644]

index 13285a5..989cb7f 100644 (file)
@@ -1255,7 +1255,7 @@ lintCoercion the_co@(NthCo n co)
        ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
            (Just (tc_s, tys_s), Just (tc_t, tys_t))
              | tc_s == tc_t
-             , isDistinctTyCon tc_s || r /= Representational
+             , isInjectiveTyCon tc_s r
                  -- see Note [NthCo and newtypes] in Coercion
              , tys_s `equalLength` tys_t
              , n < length tys_s
index 9b272cd..2db2c71 100644 (file)
@@ -459,13 +459,13 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
 -- have already been dealt with
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
           (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
-  | isDecomposableTyCon tc1
-  , isDecomposableTyCon tc2
-  = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
+  | mightBeUnsaturatedTyCon tc1
+  , mightBeUnsaturatedTyCon tc2
+  = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
            (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
-  | isDecomposableTyCon tc1
+  | mightBeUnsaturatedTyCon tc1
       -- The guard is important
       -- e.g.  (x -> y) ~ (F x y) where F has arity 1
       --       should not fail, but get the app/app case
@@ -477,7 +477,7 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _
 
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
           (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
-  | isDecomposableTyCon tc2
+  | mightBeUnsaturatedTyCon tc2
   = canEqHardFailure ev eq_rel ps_ty1 ps_ty2
 
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
@@ -622,6 +622,7 @@ can_eq_app :: CtEvidence       -- :: s1 t1 ~r s2 t2
 
 -- AppTys only decompose for nominal equality, so this case just leads
 -- to an irreducible constraint; see typecheck/should_compile/T10494
+-- See Note [Decomposing equality]
 can_eq_app ev ReprEq _ _ _ _
   = do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
        ; continueWith (CIrredEvCan { cc_ev = ev }) }
@@ -650,20 +651,17 @@ can_eq_app ev NomEq s1 t1 s2 t2
   = error "can_eq_app"
 
 ------------------------
-canDecomposableTyConApp :: CtEvidence -> EqRel
-                        -> TyCon -> [TcType]
-                        -> TyCon -> [TcType]
-                        -> TcS (StopOrContinue Ct)
+canTyConApp :: CtEvidence -> EqRel
+            -> TyCon -> [TcType]
+            -> TyCon -> [TcType]
+            -> TcS (StopOrContinue Ct)
 -- See Note [Decomposing TyConApps]
-canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
+canTyConApp ev eq_rel tc1 tys1 tc2 tys2
   | tc1 == tc2
   , length tys1 == length tys2
   = do { inerts <- getTcSInerts
-       ; if    eq_rel == NomEq      -- NomEq doesn't care about newtype vs. data
-            || isDistinctTyCon tc1  -- always good to decompose non-newtypes
-            || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
-            -- See Note [Decomposing newtypes]
-         then do { traceTcS "canDecomposableTyConApp"
+       ; if can_decompose inerts
+         then do { traceTcS "canTyConApp"
                        (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
                  ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
                  ; stopWith ev "Decomposed TyConApp" }
@@ -671,7 +669,8 @@ canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
-  | eq_rel == ReprEq && not (isDistinctTyCon tc1 && isDistinctTyCon tc2)
+  | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
+                             isGenerativeTyCon tc2 Representational)
   = canEqFailure ev eq_rel ty1 ty2
   | otherwise
   = canEqHardFailure ev eq_rel ty1 ty2
@@ -682,6 +681,11 @@ canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
     loc  = ctEvLoc ev
     pred = ctEvPred ev
 
+     -- See Note [Decomposing equality]
+    can_decompose inerts
+      =  isInjectiveTyCon tc1 (eqRelRole eq_rel)
+      || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
+
 {-
 Note [Use canEqFailure in canDecomposableTyConApp]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -734,8 +738,6 @@ NthCo on representational coercions over newtypes. NthCo comes into play
 only when decomposing givens. So we avoid decomposing representational given
 equalities over newtypes.
 
-(NB: isNewTyCon tc == True  ===>   isDistinctTyCon tc == False)
-
 But is it ever sensible to decompose *Wanted* constraints over newtypes? Yes, as
 long as there are no Givens that might (later) influence Coercible solving.
 (See Note [Instance and Given overlap] in TcInteract.) By the time we reach
@@ -759,6 +761,89 @@ evidence that (Nt Int ~R Nt Char), even if we can't form that evidence in this
 module (because Mk is not in scope). Creating this scenario in source Haskell
 is challenging; there is no test case.
 
+
+Note [Decomposing equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have a constraint (of any flavour and role) that looks like
+T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
+of course, is "it depends". This Note spells it all out.
+
+In this Note, "decomposition" refers to taking the constraint
+  [fl] (T tys1 ~X T tys2)
+(for some flavour fl and some role X) and replacing it with
+  [fls'] (tys1 ~Xs' tys2)
+where that notation indicates a list of new constraints, where the
+new constraints may have different flavours and different roles.
+
+The key property to consider is injectivity. When decomposing a Given the
+decomposition is sound if and only if T is injective in all of its type
+arguments. When decomposing a Wanted, the decomposition is sound (assuming the
+correct roles in the produced equality constraints), but it may be a guess --
+that is, an unforced decision by the constraint solver. Decomposing Wanteds
+over injective TyCons does not entail guessing. But sometimes we want to
+decompose a Wanted even when the TyCon involved is not injective! (See below.)
+
+So, in broad strokes, we want this rule:
+
+(*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
+at role X.
+
+Pursuing the details requires exploring three axes:
+* Flavour: Given vs. Derived vs. Wanted
+* Role: Nominal vs. Representational
+* TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
+
+(So a type variable isn't a TyCon, but it's convenient to put the AppTy case
+in the same table.)
+
+Right away, we can say that Derived behaves just as Wanted for the purposes
+of decomposition. The difference between Derived and Wanted is the handling of
+evidence. Since decomposition in these cases isn't a matter of soundness but of
+guessing, we want the same behavior regardless of evidence.
+
+Here is a table (discussion following) detailing where decomposition is allowed:
+
+NOMINAL               GIVEN                       WANTED
+
+Datatype               YES                         YES
+Newtype                YES                         YES
+Data family            YES                         YES
+Type family            YES, in injective args{1}   YES, in injective args{1}
+Type variable          YES                         YES
+
+REPRESENTATIONAL      GIVEN                       WANTED
+
+Datatype               YES                         YES
+Newtype                NO{2}                      MAYBE{2}
+Data family            NO{3}                      MAYBE{3}
+Type family             NO                          NO
+Type variable          NO{4}                       NO{4}
+
+{1}: Type families can be injective in some, but not all, of their arguments,
+so we want to do partial decomposition. This is quite different than the way
+other decomposition is done, where the decomposed equalities replace the original
+one. We thus proceed much like we do with superclasses: emitting new Givens
+when "decomposing" a partially-injective type family Given and new Deriveds
+when "decomposing" a partially-injective type family Wanted. (As of the time of
+writing, 13 June 2015, the implementation of injective type families has not
+been merged, but it should be soon. Please delete this parenthetical if the
+implementation is indeed merged.)
+
+{2}: See Note [Decomposing newtypes]
+
+{3}: Because of the possibility of newtype instances, we must treat data families
+like newtypes. See also Note [Decomposing newtypes].
+
+{4}: Because type variables can stand in for newtypes, we conservatively do not
+decompose AppTys over representational equality.
+
+In the implementation of can_eq_nc and friends, we don't directly pattern
+match using lines like in the tables above, as those tables don't cover
+all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
+boiling the tables above down to rule (*). The exceptions to rule (*) are for
+injective type families, which are handled separately from other decompositions,
+and the MAYBE entries above.
+
 -}
 
 canDecomposableTyConAppOK :: CtEvidence -> EqRel
@@ -1475,9 +1560,8 @@ unifyWanted loc role    orig_ty1 orig_ty2
            ; co_t <- unifyWanted loc role t1 t2
            ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) }
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-      | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
-      , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
-         -- don't look under newtypes!
+      | tc1 == tc2, tys1 `equalLength` tys2
+      , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
       = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2
            ; return (mkTcTyConAppCo role tc1 cos) }
     go (TyVarTy tv) ty2
@@ -1520,8 +1604,8 @@ unify_derived loc role    orig_ty1 orig_ty2
       = do { unify_derived loc role s1 s2
            ; unify_derived loc role t1 t2 }
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-      | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
-      , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal
+      | tc1 == tc2, tys1 `equalLength` tys2
+      , isInjectiveTyCon tc1 role
       = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
     go (TyVarTy tv) ty2
       = do { mb_ty <- isFilledMetaTyVar_maybe tv
index 415ac26..36b7947 100644 (file)
@@ -386,7 +386,7 @@ reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = impli
 ---------------
 isRigid, isRigidOrSkol :: Type -> Bool
 isRigid ty
-  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isDecomposableTyCon tc
+  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
   | Just {} <- tcSplitAppTy_maybe ty        = True
   | isForAllTy ty                           = True
   | otherwise                               = False
index 754d310..b2f31be 100644 (file)
@@ -745,7 +745,7 @@ uType origin orig_ty1 orig_ty2
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
       | tc1 == tc2, length tys1 == length tys2
-      = ASSERT( isDecomposableTyCon tc1 )
+      = ASSERT( isGenerativeTyCon tc1 Nominal )
         do { cos <- zipWithM (uType origin) tys1 tys2
            ; return $ mkTcTyConAppCo Nominal tc1 cos }
 
@@ -761,12 +761,12 @@ uType origin orig_ty1 orig_ty2
 
     go (AppTy s1 t1) (TyConApp tc2 ts2)
       | Just (ts2', t2') <- snocView ts2
-      = ASSERT( isDecomposableTyCon tc2 )
+      = ASSERT( mightBeUnsaturatedTyCon tc2 )
         go_app s1 t1 (TyConApp tc2 ts2') t2'
 
     go (TyConApp tc1 ts1) (AppTy s2 t2)
       | Just (ts1', t1') <- snocView ts1
-      = ASSERT( isDecomposableTyCon tc1 )
+      = ASSERT( mightBeUnsaturatedTyCon tc1 )
         go_app (TyConApp tc1 ts1') t1' s2 t2
 
         -- Anything else fails
index 3a55bcc..75750b4 100644 (file)
@@ -805,7 +805,7 @@ splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
 -- ^ Attempt to take a coercion application apart.
 splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
 splitAppCo_maybe (TyConAppCo r tc cos)
-  | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
+  | mightBeUnsaturatedTyCon tc || cos `lengthExceeds` tyConArity tc
   , Just (cos', co') <- snocView cos
   , Just co'' <- setNominalRole_maybe co'
   = Just (mkTyConAppCo r tc cos', co'') -- Never create unsaturated type family apps!
index 49217de..35d1781 100644 (file)
@@ -701,7 +701,7 @@ etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
   = ASSERT( tc == tc2 ) Just cos2
 
 etaTyConAppCo_maybe tc co
-  | isDecomposableTyCon tc
+  | mightBeUnsaturatedTyCon tc
   , Pair ty1 ty2     <- coercionKind co
   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
index 197e8a1..11f0c42 100644 (file)
@@ -36,7 +36,7 @@ module TyCon(
         isPrimTyCon,
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
         isTypeSynonymTyCon,
-        isDecomposableTyCon,
+        mightBeUnsaturatedTyCon,
         isPromotedDataCon, isPromotedTyCon,
         isPromotedDataCon_maybe, isPromotedTyCon_maybe,
         promotableTyCon_maybe, promoteTyCon,
@@ -49,7 +49,7 @@ module TyCon(
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
         isBuiltInSynFamTyCon_maybe,
         isUnLiftedTyCon,
-        isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
+        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isDistinctAlgRhs,
         isTyConAssoc, tyConAssoc_maybe,
         isRecursiveTyCon,
         isImplicitTyCon,
@@ -1210,21 +1210,33 @@ isDataTyCon (AlgTyCon {algTcRhs = rhs})
         AbstractTyCon {}   -> False      -- We don't know, so return False
 isDataTyCon _ = False
 
--- | 'isDistinctTyCon' is true of 'TyCon's that are equal only to
--- themselves, even via representational coercions (except for unsafeCoerce).
--- This excludes newtypes, type functions, type synonyms.
--- It relates directly to the FC consistency story:
---     If the axioms are consistent,
---     and  co : S tys ~R T tys, and S,T are "distinct" TyCons,
---     then S=T.
--- Cf Note [Pruning dead case alternatives] in Unify
-isDistinctTyCon :: TyCon -> Bool
-isDistinctTyCon (AlgTyCon {algTcRhs = rhs}) = isDistinctAlgRhs rhs
-isDistinctTyCon (FunTyCon {})               = True
-isDistinctTyCon (PrimTyCon {})              = True
-isDistinctTyCon (PromotedDataCon {})        = True
-isDistinctTyCon _                           = False
-
+-- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
+-- (where X is the role passed in):
+--   If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
+-- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
+isInjectiveTyCon :: TyCon -> Role -> Bool
+isInjectiveTyCon _                             Phantom          = False
+isInjectiveTyCon (FunTyCon {})                 _                = True
+isInjectiveTyCon (AlgTyCon {})                 Nominal          = True
+isInjectiveTyCon (AlgTyCon {algTcRhs = rhs})   Representational
+  = isDistinctAlgRhs rhs
+isInjectiveTyCon (SynonymTyCon {})             _                = False
+isInjectiveTyCon (FamilyTyCon {})              _                = False
+isInjectiveTyCon (PrimTyCon {})                _                = True
+isInjectiveTyCon (PromotedDataCon {})          _                = True
+isInjectiveTyCon (PromotedTyCon {ty_con = tc}) r
+  = isInjectiveTyCon tc r
+
+-- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
+-- (where X is the role passed in):
+--   If (T tys ~X t), then (t's head ~X T).
+isGenerativeTyCon :: TyCon -> Role -> Bool
+isGenerativeTyCon = isInjectiveTyCon
+  -- as it happens, generativity and injectivity coincide, but there's
+  -- no a priori reason this must be the case
+
+-- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
+-- with respect to representational equality?
 isDistinctAlgRhs :: AlgTyConRhs -> Bool
 isDistinctAlgRhs (TupleTyCon {})          = True
 isDistinctAlgRhs (DataTyCon {})           = True
@@ -1317,17 +1329,17 @@ isTypeSynonymTyCon _                 = False
 -- right hand side to which a synonym family application can expand.
 --
 
-isDecomposableTyCon :: TyCon -> Bool
+mightBeUnsaturatedTyCon :: TyCon -> Bool
 -- True iff we can decompose (T a b c) into ((T a b) c)
 --   I.e. is it injective and generative w.r.t nominal equality?
 -- Specifically NOT true of synonyms (open and otherwise)
 --
--- It'd be unusual to call isDecomposableTyCon on a regular H98
+-- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
 -- type synonym, because you should probably have expanded it first
 -- But regardless, it's not decomposable
-isDecomposableTyCon (SynonymTyCon {}) = False
-isDecomposableTyCon (FamilyTyCon  {}) = False
-isDecomposableTyCon _other            = True
+mightBeUnsaturatedTyCon (SynonymTyCon {}) = False
+mightBeUnsaturatedTyCon (FamilyTyCon  {}) = False
+mightBeUnsaturatedTyCon _other            = True
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
index 41b6b2d..74cc667 100644 (file)
@@ -392,7 +392,7 @@ repSplitAppTy_maybe (FunTy ty1 ty2)
   | otherwise                         = Just (TyConApp funTyCon [ty1], ty2)
 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 repSplitAppTy_maybe (TyConApp tc tys)
-  | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc
+  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
   , Just (tys', ty') <- snocView tys
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 repSplitAppTy_maybe _other = Nothing
@@ -415,8 +415,8 @@ splitAppTys ty = split ty ty []
     split _       (AppTy ty arg)        args = split ty ty (arg:args)
     split _       (TyConApp tc tc_args) args
       = let -- keep type families saturated
-            n | isDecomposableTyCon tc = 0
-              | otherwise              = tyConArity tc
+            n | mightBeUnsaturatedTyCon tc = 0
+              | otherwise                  = tyConArity tc
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
diff --git a/testsuite/tests/typecheck/should_compile/RepArrow.hs b/testsuite/tests/typecheck/should_compile/RepArrow.hs
new file mode 100644 (file)
index 0000000..d891387
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module RepArrow where
+
+import Data.Ord ( Down )  -- convenient "Id" newtype, without its constructor
+import Data.Coerce
+
+foo :: Coercible (Down (Int -> Int)) (Int -> Int) => ()
+foo = ()