Use a Representaional coercion for data families
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 24 Jun 2015 21:35:32 +0000 (22:35 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 Jun 2015 07:33:04 +0000 (08:33 +0100)
When we have
  data instance T (a,b) = MkT a b
we make a represntation type
  data TPair a b = MkT a b
plus an axiom to connect the two
  ax a b :: T (a,b)  ~R  TPair a b

Previously this was a Nominal equality, and that worked ok
but seems illogical since Nominal equalities are between
types that the programmer thinks of as being equal.  But
TPair is not visible to the programmer; indeed we call it
the "representation TyCon".  So a Representational equality
seems more suitable here.

12 files changed:
compiler/hsSyn/HsUtils.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcGenGenerics.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcUnify.hs
compiler/types/FamInstEnv.hs
compiler/types/TyCon.hs
compiler/vectorise/Vectorise/Generic/PAMethods.hs
compiler/vectorise/Vectorise/Generic/PData.hs

index fd3d5ef..2242d10 100644 (file)
@@ -23,7 +23,7 @@ module HsUtils(
   mkSimpleMatch, unguardedGRHSs, unguardedRHS,
   mkMatchGroup, mkMatchGroupName, mkMatch, mkHsLam, mkHsIf,
   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
-  coToHsWrapper, mkHsDictLet, mkHsLams,
+  coToHsWrapper, coToHsWrapperR, mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
   mkLHsPar, mkHsCmdCast,
 
@@ -477,11 +477,11 @@ mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
 mkHsWrap co_fn e | isIdHsWrapper co_fn = e
                  | otherwise           = HsWrap co_fn e
 
-mkHsWrapCo :: TcCoercion   -- A Nominal coercion  a ~N b
+mkHsWrapCo :: TcCoercionN   -- A Nominal coercion  a ~N b
            -> HsExpr id -> HsExpr id
 mkHsWrapCo co e = mkHsWrap (coToHsWrapper co) e
 
-mkHsWrapCoR :: TcCoercion   -- A Representational coercion  a ~R b
+mkHsWrapCoR :: TcCoercionR   -- A Representational coercion  a ~R b
             -> HsExpr id -> HsExpr id
 mkHsWrapCoR co e = mkHsWrap (coToHsWrapperR co) e
 
index bdc6794..684ab4f 100644 (file)
@@ -223,6 +223,7 @@ tcInstNewTyCon_maybe tc tys = fmap (second TcCoercion) $
 
 -- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
 -- there is no data family to unwrap.
+-- Returns a Representational coercion
 tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
                     -> (TyCon, [TcType], Coercion)
 tcLookupDataFamInst fam_inst_envs tc tc_args
index dfe8385..e08d0d5 100644 (file)
@@ -20,7 +20,8 @@ module TcEvidence (
   EvTypeable(..),
 
   -- TcCoercion
-  TcCoercion(..), LeftOrRight(..), pickLR,
+  TcCoercion(..), TcCoercionR, TcCoercionN,
+  LeftOrRight(..), pickLR,
   mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
   mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
@@ -134,6 +135,9 @@ the arguments tends to be to hand at call sites, so it's quicker than
 using, say, tcCoercionKind.
 -}
 
+type TcCoercionN = TcCoercion    -- A Nominal          corecion ~N
+type TcCoercionR = TcCoercion    -- A Representational corecion ~R
+
 data TcCoercion
   = TcRefl Role TcType
   | TcTyConAppCo Role TyCon [TcCoercion]
@@ -150,7 +154,7 @@ data TcCoercion
   | TcTransCo TcCoercion TcCoercion
   | TcNthCo Int TcCoercion
   | TcLRCo LeftOrRight TcCoercion
-  | TcSubCo TcCoercion
+  | TcSubCo TcCoercion                 -- Argument is never TcRefl
   | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
   | TcLetCo TcEvBinds TcCoercion
   | TcCoercion Coercion            -- embed a Core Coercion
@@ -196,12 +200,15 @@ mkTcTyConAppCo role tc cos -- No need to expand type synonyms
 
   | otherwise = TcTyConAppCo role tc cos
 
--- input coercion is Nominal
+-- Input coercion is Nominal
 -- mkSubCo will do some normalisation. We do not do it for TcCoercions, but
 -- defer that to desugaring; just to reduce the code duplication a little bit
 mkTcSubCo :: TcCoercion -> TcCoercion
-mkTcSubCo co = ASSERT2( tcCoercionRole co == Nominal, ppr co)
-               TcSubCo co
+mkTcSubCo (TcRefl _ ty)
+  = TcRefl Representational ty
+mkTcSubCo co
+   = ASSERT2( tcCoercionRole co == Nominal, ppr co)
+     TcSubCo co
 
 -- See Note [Role twiddling functions] in Coercion
 -- | Change the role of a 'TcCoercion'. Returns 'Nothing' if this isn't
index 7b47fcf..397834a 100644 (file)
@@ -1201,7 +1201,7 @@ tcTagToEnum loc fun_name arg res_ty
         -- Look through any type family
         ; fam_envs <- tcGetFamInstEnvs
         ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args
-             -- coi :: tc tc_args ~ rep_tc rep_args
+             -- coi :: tc tc_args ~R rep_tc rep_args
 
         ; checkTc (isEnumerationTyCon rep_tc)
                   (mk_error ty' doc2)
index 649aa5f..63fee7f 100644 (file)
@@ -506,7 +506,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
                    in newGlobalBinder mod (mkGen (nameOccName (tyConName tycon)))
                         (nameSrcSpan (tyConName tycon))
 
-     ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy
+     ; let axiom = mkSingleCoAxiom Nominal rep_name tyvars fam_tc appT repTy
      ; newFamInst SynFamilyInst axiom  }
 
 --------------------------------------------------------------------------------
index c815d2d..9a0093d 100644 (file)
@@ -571,7 +571,7 @@ tcATDefault inst_subst defined_ats (ATI fam_tc defs)
              tv_set'  = tyVarsOfTypes pat_tys'
              tvs'     = varSetElemsKvsFirst tv_set'
        ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
-       ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
+       ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' fam_tc pat_tys' rhs'
        ; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
                                               , pprCoAxiom axiom ])
        ; fam_inst <- ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' )
@@ -699,7 +699,8 @@ tcDataFamInstDecl mb_clsinfo
                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
               -- freshen tyvars
               ; let (eta_tvs, eta_pats) = eta_reduce tvs' pats'
-                    axiom    = mkSingleCoAxiom axiom_name eta_tvs fam_tc eta_pats
+                    axiom    = mkSingleCoAxiom Representational
+                                               axiom_name eta_tvs fam_tc eta_pats
                                                (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                     parent   = FamInstTyCon axiom fam_tc pats'
                     roles    = map (const Nominal) tvs'
index 7aafdf5..f04ab9e 100644 (file)
@@ -566,7 +566,7 @@ tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
 ------------------------
 -- Lists, tuples, arrays
 tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
-  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy pat_ty
+  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res)
@@ -575,14 +575,14 @@ tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
 tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
   = do  { list_pat_ty <- newFlexiTyVarTy liftedTypeKind
         ; e' <- tcSyntaxOp ListOrigin e (mkFunTy pat_ty list_pat_ty)
-        ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy list_pat_ty
+        ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR list_pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (ListPat pats' elt_ty (Just (pat_ty,e'))) list_pat_ty, res)
         }
 
 tc_pat penv (PArrPat pats _) pat_ty thing_inside
-  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy pat_ty
+  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTyR pat_ty
         ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                      pats penv thing_inside
         ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
@@ -590,7 +590,7 @@ tc_pat penv (PArrPat pats _) pat_ty thing_inside
 
 tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
   = do  { let tc = tupleTyCon boxity (length pats)
-        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) pat_ty
+        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConAppR tc) pat_ty
         ; (pats', res) <- tc_lpats penv pats arg_tys thing_inside
 
         ; dflags <- getDynFlags
@@ -904,14 +904,27 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
         ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
 
 ----------------------------
-matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercion, a))
+downgrade :: (TcRhoType -> TcM (TcCoercionN, a))
+          -> TcRhoType -> TcM (TcCoercionR, a)
+downgrade f a = do { (co,res) <- f a; return (mkTcSubCo co, res) }
+
+matchExpectedListTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType)
+matchExpectedListTyR = downgrade matchExpectedListTy
+matchExpectedPArrTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType)
+matchExpectedPArrTyR = downgrade matchExpectedPArrTy
+matchExpectedTyConAppR :: TyCon -> TcRhoType -> TcM (TcCoercionR, [TcSigmaType])
+matchExpectedTyConAppR tc = downgrade (matchExpectedTyConApp tc)
+
+----------------------------
+matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionR, a))
                     -> TcRhoType -> TcM (HsWrapper, a)
 -- See Note [Matching polytyped patterns]
--- Returns a wrapper : pat_ty ~ inner_ty
+-- Returns a wrapper : pat_ty ~R inner_ty
 matchExpectedPatTy inner_match pat_ty
   | null tvs && null theta
-  = do { (co, res) <- inner_match pat_ty
-       ; return (coToHsWrapper (mkTcSymCo co), res) }
+  = do { (co, res) <- inner_match pat_ty   -- 'co' is Representational
+       ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr co $$ ppr (isTcReflCo co))
+       ; return (coToHsWrapperR (mkTcSymCo co), res) }
          -- The Sym is because the inner_match returns a coercion
          -- that is the other way round to matchExpectedPatTy
 
@@ -927,7 +940,7 @@ matchExpectedPatTy inner_match pat_ty
 matchExpectedConTy :: TyCon      -- The TyCon that this data
                                  -- constructor actually returns
                    -> TcRhoType  -- The type of the pattern
-                   -> TcM (TcCoercion, [TcSigmaType])
+                   -> TcM (TcCoercionR, [TcSigmaType])
 -- See Note [Matching constructor patterns]
 -- Returns a coercion : T ty1 ... tyn ~ pat_ty
 -- This is the same way round as matchExpectedListTy etc
@@ -943,17 +956,17 @@ matchExpectedConTy data_tc pat_ty
                                              ppr (tyConTyVars data_tc),
                                              ppr fam_tc, ppr fam_args])
        ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
-             -- co1 : T (ty1,ty2) ~ pat_ty
+             -- co1 : T (ty1,ty2) ~N pat_ty
 
        ; let tys' = mkTyVarTys tvs'
-             co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys'
-             -- co2 : T (ty1,ty2) ~ T7 ty1 ty2
+             co2 = mkTcUnbranchedAxInstCo Representational co_tc tys'
+             -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
 
-       ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys') }
+       ; return (mkTcSymCo co2 `mkTcTransCo` mkTcSubCo co1, tys') }
 
   | otherwise
-  = matchExpectedTyConApp data_tc pat_ty
-             -- coi : T tys ~ pat_ty
+  = matchExpectedTyConAppR data_tc pat_ty
+             -- coi : T tys ~R pat_ty
 
 {-
 Note [Matching constructor patterns]
index 3f540f5..2e3834e 100644 (file)
@@ -107,10 +107,10 @@ expected type, because it expects that to have been done already
 matchExpectedFunTys :: SDoc     -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
                     -> TcRhoType
-                    -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
+                    -> TcM (TcCoercionN, [TcSigmaType], TcRhoType)
 
 -- If    matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
--- then  co : ty ~ (t1 -> ... -> tn -> ty_r)
+-- then  co : ty ~N (t1 -> ... -> tn -> ty_r)
 --
 -- Does not allocate unnecessary meta variables: if the input already is
 -- a function, we just take it apart.  Not only is this efficient,
@@ -205,14 +205,14 @@ we are ok.
 -}
 
 ----------------------
-matchExpectedListTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
+matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
 -- Special case for lists
 matchExpectedListTy exp_ty
  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
       ; return (co, elt_ty) }
 
 ----------------------
-matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
+matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
 -- Special case for parrs
 matchExpectedPArrTy exp_ty
   = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
@@ -221,7 +221,7 @@ matchExpectedPArrTy exp_ty
 ---------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType            -- orig_ty
-                      -> TcM (TcCoercion,     -- T k1 k2 k3 a b c ~ orig_ty
+                      -> TcM (TcCoercionN,    -- T k1 k2 k3 a b c ~N orig_ty
                               [TcSigmaType])  -- Element types, k1 k2 k3 a b c
 
 -- It's used for wired-in tycons, so we call checkWiredInTyCon
index ee92996..6c54b57 100644 (file)
@@ -551,12 +551,17 @@ mkUnbranchedCoAxiom ax_name fam_tc branch
             , co_ax_implicit = False
             , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
 
-mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched
-mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty
+mkSingleCoAxiom :: Role -> Name
+                -> [TyVar] -> TyCon -> [Type] -> Type
+                -> CoAxiom Unbranched
+-- Make a single-branch CoAxiom, incluidng making the branch itself
+-- Used for both type family (Nominal) and data family (Representational)
+-- axioms, hence passing in the Role
+mkSingleCoAxiom role ax_name tvs fam_tc lhs_tys rhs_ty
   = CoAxiom { co_ax_unique   = nameUnique ax_name
             , co_ax_name     = ax_name
             , co_ax_tc       = fam_tc
-            , co_ax_role     = Nominal
+            , co_ax_role     = role
             , co_ax_implicit = False
             , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
   where
index e1cd128..c572828 100644 (file)
@@ -177,8 +177,9 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
 
         data T a
         data R:TInt = T1 | T2 Bool
-        axiom ax_ti : T Int ~ R:TInt
+        axiom ax_ti : T Int ~R R:TInt
 
+  Note that this is a *representational* coercion
   The R:TInt is the "representation TyCons".
   It has an AlgTyConParent of
         FamInstTyCon T [Int] ax_ti
@@ -203,7 +204,7 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
         data R:TPair a where
           X1 :: R:TPair Int Bool
           X2 :: a -> b -> R:TPair a b
-        axiom ax_pr :: T (a,b) ~ R:TPair a b
+        axiom ax_pr :: T (a,b)  ~R  R:TPair a b
 
         $WX1 :: forall a b. a -> b -> T (a,b)
         $WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
@@ -652,7 +653,8 @@ data TyConParent
   --  type with the type instance family
   | FamInstTyCon          -- See Note [Data type families]
         (CoAxiom Unbranched)  -- The coercion axiom.
-               -- Generally of kind   T ty1 ty2 ~ R:T a b c
+               -- A *Representational* coercion,
+               -- of kind   T ty1 ty2   ~R   R:T a b c
                -- where T is the family TyCon,
                -- and R:T is the representation TyCon (ie this one)
                -- and a,b,c are the tyConTyVars of this TyCon
index 2f4e23e..b5626bd 100644 (file)
@@ -38,7 +38,7 @@ buildPReprTyCon orig_tc vect_tc repr
  = do name      <- mkLocalisedName mkPReprTyConOcc (tyConName orig_tc)
       rhs_ty    <- sumReprType repr
       prepr_tc  <- builtin preprTyCon
-      let axiom = mkSingleCoAxiom name tyvars prepr_tc instTys rhs_ty
+      let axiom = mkSingleCoAxiom Nominal name tyvars prepr_tc instTys rhs_ty
       liftDs $ newFamInst SynFamilyInst axiom
   where
     tyvars = tyConTyVars vect_tc
index 387d49c..ed127b4 100644 (file)
@@ -46,7 +46,7 @@ buildDataFamInst name' fam_tc vect_tc rhs
  = do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
 
       ; (_, tyvars') <- liftDs $ tcInstSigTyVarsLoc (getSrcSpan name') tyvars
-      ; let ax       = mkSingleCoAxiom axiom_name tyvars' fam_tc pat_tys rep_ty
+      ; let ax       = mkSingleCoAxiom Representational axiom_name tyvars' fam_tc pat_tys rep_ty
             tys'     = mkTyVarTys tyvars'
             rep_ty   = mkTyConApp rep_tc tys'
             pat_tys  = [mkTyConApp vect_tc tys']