Updated documentation; changed "group" to "branched" in type families
[ghc.git] / compiler / types / OptCoercion.lhs
index e6f3b56..7eaab5c 100644 (file)
@@ -1,15 +1,24 @@
-%\r
-% (c) The University of Glasgow 2006\r
-%\r
-\r
-\begin{code}\r
-module OptCoercion ( optCoercion ) where 
+%
+% (c) The University of Glasgow 2006
+%
+
+\begin{code}
+{-# OPTIONS -fno-warn-tabs #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and
+-- detab the module (please do the detabbing in a separate patch). See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
+-- for details
+
+module OptCoercion ( optCoercion, checkAxInstCo ) where 
 
 #include "HsVersions.h"
 
 import Coercion
 import Type hiding( substTyVarBndr, substTy, extendTvSubst )
+import TcType       ( exactTyVarsOfType )
 import TyCon
+import CoAxiom
 import Var
 import VarSet
 import VarEnv
@@ -18,6 +27,9 @@ import Outputable
 import Pair
 import Maybes( allMaybes )
 import FastString
+import Util
+import Unify
+import InstEnv
 \end{code}
 
 %************************************************************************
@@ -110,12 +122,12 @@ opt_co' env sym (CoVarCo cv)
                 ASSERT( isCoVar cv )
                 wrapSym sym (CoVarCo cv)
 
-opt_co' env sym (AxiomInstCo con cos)
+opt_co' env sym (AxiomInstCo con ind cos)
     -- Do *not* push sym inside top-level axioms
     -- e.g. if g is a top-level axiom
     --   g a : f a ~ a
     -- then (sym (g ty)) /= g (sym ty) !!
-  = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)
+  = wrapSym sym $ AxiomInstCo con ind (map (opt_co env False) cos)
       -- Note that the_co does *not* have sym pushed into it
 
 opt_co' env sym (UnsafeCo ty1 ty2)
@@ -127,15 +139,16 @@ opt_co' env sym (UnsafeCo ty1 ty2)
     ty2' = substTy env ty2
 
 opt_co' env sym (TransCo co1 co2)
-  | sym       = opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
-  | otherwise = opt_trans opt_co1 opt_co2
+  | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
+  | otherwise = opt_trans in_scope opt_co1 opt_co2
   where
     opt_co1 = opt_co env sym co1
     opt_co2 = opt_co env sym co2
+    in_scope = getCvInScope env
 
 opt_co' env sym (NthCo n co)
   | TyConAppCo tc cos <- co'
-  , isDecomposableTyCon tc             -- Not synonym families
+  , isDecomposableTyCon tc   -- Not synonym families
   = ASSERT( n < length cos )
     cos !! n
   | otherwise
@@ -143,181 +156,277 @@ opt_co' env sym (NthCo n co)
   where
     co' = opt_co env sym co
 
+opt_co' env sym (LRCo lr co)
+  | Just pr_co <- splitAppCo_maybe co'
+  = pickLR lr pr_co
+  | otherwise
+  = LRCo lr co'
+  where
+    co' = opt_co env sym co
+
 opt_co' env sym (InstCo co ty)
     -- See if the first arg is already a forall
     -- ...then we can just extend the current substitution
   | Just (tv, co_body) <- splitForAllCo_maybe co
   = opt_co (extendTvSubst env tv ty') sym co_body
 
-    -- See if it is a forall after optimization
+     -- See if it is a forall after optimization
+     -- If so, do an inefficient one-variable substitution
   | Just (tv, co'_body) <- splitForAllCo_maybe co'
-  = substCoWithTy tv ty' co'_body   -- An inefficient one-variable substitution
+  = substCoWithTy (getCvInScope env) tv ty' co'_body   
 
   | otherwise = InstCo co' ty'
-
   where
     co' = opt_co env sym co
     ty' = substTy env ty
 
 -------------
-opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]
-opt_transList = zipWith opt_trans
+opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
+opt_transList is = zipWith (opt_trans is)
 
-opt_trans :: NormalCo -> NormalCo -> NormalCo
-opt_trans co1 co2
+opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+opt_trans is co1 co2
   | isReflCo co1 = co2
-  | otherwise    = opt_trans1 co1 co2
+  | otherwise    = opt_trans1 is co1 co2
 
-opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
 -- First arg is not the identity
-opt_trans1 co1 co2
+opt_trans1 is co1 co2
   | isReflCo co2 = co1
-  | otherwise    = opt_trans2 co1 co2
+  | otherwise    = opt_trans2 is co1 co2
 
-opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
 -- Neither arg is the identity
-opt_trans2 (TransCo co1a co1b) co2
+opt_trans2 is (TransCo co1a co1b) co2
     -- Don't know whether the sub-coercions are the identity
-  = opt_trans co1a (opt_trans co1b co2)  
+  = opt_trans is co1a (opt_trans is co1b co2)  
 
-opt_trans2 co1 co2 
-  | Just co <- opt_trans_rule co1 co2
+opt_trans2 is co1 co2 
+  | Just co <- opt_trans_rule is co1 co2
   = co
 
-opt_trans2 co1 (TransCo co2a co2b)
-  | Just co1_2a <- opt_trans_rule co1 co2a
+opt_trans2 is co1 (TransCo co2a co2b)
+  | Just co1_2a <- opt_trans_rule is co1 co2a
   = if isReflCo co1_2a
     then co2b
-    else opt_trans1 co1_2a co2b
+    else opt_trans1 is co1_2a co2b
 
-opt_trans2 co1 co2
+opt_trans2 co1 co2
   = mkTransCo co1 co2
 
 ------
 -- Optimize coercions with a top-level use of transitivity.
-opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
-
--- push transitivity down through matching top-level constructors.
-opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
-  | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
-                 TyConAppCo tc1 (opt_transList cos1 cos2)
+opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
 
--- push transitivity through matching destructors
-opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+-- Push transitivity through matching destructors
+opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
   | d1 == d2
   , co1 `compatible_co` co2
   = fireTransRule "PushNth" in_co1 in_co2 $
-    mkNthCo d1 (opt_trans co1 co2)
+    mkNthCo d1 (opt_trans is co1 co2)
+
+opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2
+  = fireTransRule "PushLR" in_co1 in_co2 $
+    mkLRCo d1 (opt_trans is co1 co2)
 
 -- Push transitivity inside instantiation
-opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
   | ty1 `eqType` ty2
   , co1 `compatible_co` co2
   = fireTransRule "TrPushInst" in_co1 in_co2 $
-    mkInstCo (opt_trans co1 co2) ty1
+    mkInstCo (opt_trans is co1 co2) ty1
  
--- Push transitivity inside apply
-opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+-- Push transitivity down through matching top-level constructors.
+opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
+  | tc1 == tc2 
+  = fireTransRule "PushTyConApp" in_co1 in_co2 $
+    TyConAppCo tc1 (opt_transList is cos1 cos2)
+
+opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
   = fireTransRule "TrPushApp" in_co1 in_co2 $
-    mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)
+    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
 
-opt_trans_rule co1@(TyConAppCo tc cos1) co2
+-- Eta rules
+opt_trans_rule is co1@(TyConAppCo tc cos1) co2
   | Just cos2 <- etaTyConAppCo_maybe tc co2
   = ASSERT( length cos1 == length cos2 )
     fireTransRule "EtaCompL" co1 co2 $
-    TyConAppCo tc (zipWith opt_trans cos1 cos2)
+    TyConAppCo tc (opt_transList is cos1 cos2)
 
-opt_trans_rule co1 co2@(TyConAppCo tc cos2)
+opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
   | Just cos1 <- etaTyConAppCo_maybe tc co1
   = ASSERT( length cos1 == length cos2 )
     fireTransRule "EtaCompR" co1 co2 $
-    TyConAppCo tc (zipWith opt_trans cos1 cos2)
+    TyConAppCo tc (opt_transList is cos1 cos2)
+
+opt_trans_rule is co1@(AppCo co1a co1b) co2
+  | Just (co2a,co2b) <- etaAppCo_maybe co2
+  = fireTransRule "EtaAppL" co1 co2 $
+    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+
+opt_trans_rule is co1 co2@(AppCo co2a co2b)
+  | Just (co1a,co1b) <- etaAppCo_maybe co1
+  = fireTransRule "EtaAppR" co1 co2 $
+    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
 
 -- Push transitivity inside forall
-opt_trans_rule co1 co2
+opt_trans_rule is co1 co2
   | Just (tv1,r1) <- splitForAllCo_maybe co1
   , Just (tv2,r2) <- etaForAllCo_maybe co2
-  , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2
+  , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
+        is' = is `extendInScopeSet` tv1
   = fireTransRule "EtaAllL" co1 co2 $
-    mkForAllCo tv1 (opt_trans2 r1 r2')
+    mkForAllCo tv1 (opt_trans2 is' r1 r2')
 
   | Just (tv2,r2) <- splitForAllCo_maybe co2
   , Just (tv1,r1) <- etaForAllCo_maybe co1
-  , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1
+  , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
+        is' = is `extendInScopeSet` tv2
   = fireTransRule "EtaAllR" co1 co2 $
-    mkForAllCo tv1 (opt_trans2 r1' r2)
+    mkForAllCo tv1 (opt_trans2 is' r1' r2)
 
 -- Push transitivity inside axioms
-opt_trans_rule co1 co2
-
-  -- TrPushAxR/TrPushSymAxR
-  | Just (sym, con, cos1) <- co1_is_axiom_maybe
-  , Just cos2 <- matchAxiom sym con co2
-  = fireTransRule "TrPushAxR" co1 co2 $
-    if sym 
-    then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)
-    else         AxiomInstCo con (opt_transList cos1 cos2)
-
-  -- TrPushAxL/TrPushSymAxL
-  | Just (sym, con, cos2) <- co2_is_axiom_maybe
-  , Just cos1 <- matchAxiom (not sym) con co1
-  = fireTransRule "TrPushAxL" co1 co2 $
-    if sym 
-    then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))
-    else         AxiomInstCo con (opt_transList cos1 cos2)
+opt_trans_rule is co1 co2
+
+  -- TrPushSymAxR
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , Just cos2 <- matchAxiom sym con ind co2
+  , True <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
+
+  -- TrPushAxR
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , Just cos2 <- matchAxiom sym con ind co2
+  , False <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushAxR" co1 co2 newAxInst
+
+  -- TrPushSymAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , True <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
+
+  -- TrPushAxL  
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , False <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushAxL" co1 co2 newAxInst
 
   -- TrPushAxSym/TrPushSymAx
-  | Just (sym1, con1, cos1) <- co1_is_axiom_maybe
-  , Just (sym2, con2, cos2) <- co2_is_axiom_maybe
+  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
+  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
   , con1 == con2
+  , ind1 == ind2
   , sym1 == not sym2
-  , let qtvs = co_ax_tvs con1
-        lhs  = co_ax_lhs con1 
-        rhs  = co_ax_rhs con1 
+  , let branch = coAxiomNthBranch con1 ind1
+        qtvs = coAxBranchTyVars branch
+        lhs  = coAxNthLHS con1 ind1
+        rhs  = coAxBranchRHS branch
         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
   , all (`elemVarSet` pivot_tvs) qtvs
   = fireTransRule "TrPushAxSym" co1 co2 $
     if sym2
-    then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
-    else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
+    then liftCoSubstWith qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
+    else liftCoSubstWith qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
   where
     co1_is_axiom_maybe = isAxiom_maybe co1
     co2_is_axiom_maybe = isAxiom_maybe co2
 
-opt_trans_rule co1 co2 -- Identity rule
+opt_trans_rule _ co1 co2       -- Identity rule
   | Pair ty1 _ <- coercionKind co1
   , Pair _ ty2 <- coercionKind co2
   , ty1 `eqType` ty2
   = fireTransRule "RedTypeDirRefl" co1 co2 $
     Refl ty2
 
-opt_trans_rule _ _ = Nothing
+opt_trans_rule _ _ = Nothing
 
 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
 fireTransRule _rule _co1 _co2 res
   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
     Just res
 
+\end{code}
+
+Note [Conflict checking with AxiomInstCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following type family and axiom:
+
+type family Equal (a :: k) (b :: k) :: Bool
+type instance where
+  Equal a a = True
+  Equal a b = False
+--
+Equal :: forall k::BOX. k -> k -> Bool
+axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
+           ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
+
+We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 0-based,
+so this is the second branch of the axiom.) The problem is that, on the surface, it
+seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that all is
+OK. But, all is not OK: we want to use the first branch of the axiom in this case,
+not the second. The problem is that the parameters of the first branch can unify with
+the supplied coercions, thus meaning that the first branch should be taken. See also
+Note [Branched instance checking] in types/FamInstEnv.lhs.
+
+\begin{code}
+-- | Check to make sure that an AxInstCo is internally consistent.
+-- Returns the number of the conflicting branch, if it exists
+-- See Note [Conflict checking with AxiomInstCo]
+checkAxInstCo :: Coercion -> Maybe Int
+-- defined here to avoid dependencies in Coercion
+checkAxInstCo (AxiomInstCo ax ind cos)
+  = let branch = coAxiomNthBranch ax ind
+        tvs = coAxBranchTyVars branch
+        tys = map (pFst . coercionKind) cos 
+        subst = zipOpenTvSubst tvs tys
+        lhs' = Type.substTys subst (coAxBranchLHS branch) in
+    check_no_conflict lhs' (ind-1)
+  where
+    check_no_conflict :: [Type] -> Int -> Maybe Int
+    check_no_conflict _ (-1) = Nothing
+    check_no_conflict lhs' j
+      | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj
+      = check_no_conflict lhs' (j-1)
+      | otherwise
+      = Just j
+      where
+        (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch ax j
+checkAxInstCo _ = Nothing
+
 -----------
 wrapSym :: Bool -> Coercion -> Coercion
 wrapSym sym co | sym       = SymCo co
                | otherwise = co
 
 -----------
-isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])
+isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
 isAxiom_maybe (SymCo co) 
-  | Just (sym, con, cos) <- isAxiom_maybe co
-  = Just (not sym, con, cos)
-isAxiom_maybe (AxiomInstCo con cos)
-  = Just (False, con, cos)
+  | Just (sym, con, ind, cos) <- isAxiom_maybe co
+  = Just (not sym, con, ind, cos)
+isAxiom_maybe (AxiomInstCo con ind cos)
+  = Just (False, con, ind, cos)
 isAxiom_maybe _ = Nothing
 
 matchAxiom :: Bool -- True = match LHS, False = match RHS
-           -> CoAxiom -> Coercion -> Maybe [Coercion]
+           -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
 -- If we succeed in matching, then *all the quantified type variables are bound*
 -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
-matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co
-  = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of
+matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
+  = let (CoAxBranch { cab_tvs = qtvs
+                    , cab_lhs = lhs
+                    , cab_rhs = rhs }) = coAxiomNthBranch ax ind in
+    case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
       Nothing    -> Nothing
       Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
 
@@ -346,6 +455,21 @@ etaForAllCo_maybe co
   | otherwise
   = Nothing
 
+etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
+-- If possible, split a coercion
+--   g :: t1a t1b ~ t2a t2b
+-- into a pair of coercions (left g, right g)
+etaAppCo_maybe co
+  | Just (co1,co2) <- splitAppCo_maybe co
+  = Just (co1,co2)
+  | Pair ty1 ty2 <- coercionKind co
+  , Just (_,t1) <- splitAppTy_maybe ty1
+  , Just (_,t2) <- splitAppTy_maybe ty2
+  , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
+  = Just (LRCo CLeft co, LRCo CRight co)
+  | otherwise
+  = Nothing
+
 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
 -- If possible, split a coercion 
 --       g :: T s1 .. sn ~ T t1 .. tn
@@ -370,3 +494,25 @@ etaTyConAppCo_maybe tc co
   | otherwise
   = Nothing
 \end{code}  
+
+Note [Eta for AppCo]
+~~~~~~~~~~~~~~~~~~~~
+Suppose we have 
+   g :: s1 t1 ~ s2 t2
+
+Then we can't necessarily make
+   left  g :: s1 ~ s2
+   right g :: t1 ~ t2
+because it's possible that
+   s1 :: * -> *         t1 :: *
+   s2 :: (*->*) -> *    t2 :: * -> *
+and in that case (left g) does not have the same
+kind on either side.
+
+It's enough to check that 
+  kind t1 = kind t2
+because if g is well-kinded then
+  kind (s1 t2) = kind (s2 t2)
+and these two imply
+  kind s1 = kind s2
+