+type NormalCo = Coercion
+ -- Invariants:
+ -- * For trans coercions (co1 `trans` co2)
+ -- co1 is not a trans, and neither co1 nor co2 is identity
+ -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
+
+type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
+
+optCoercion :: Coercion -> NormalCo
+optCoercion co = opt_co False co
+
+opt_co :: Bool -- True <=> return (sym co)
+ -> Coercion
+ -> NormalCo
+opt_co = opt_co'
+-- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
+-- co1 `seq`
+-- pprTrace "opt_co done }" (ppr co1)
+-- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1)
+-- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
+-- co1
+-- where
+-- co1 = opt_co' sym co
+-- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
+-- (s,t) = coercionKind co
+-- (s1,t1) | sym = (t,s)
+-- | otherwise = (s,t)
+-- (s2,t2) = coercionKind co1
+
+opt_co' sym (AppTy ty1 ty2) = mkAppTy (opt_co sym ty1) (opt_co sym ty2)
+opt_co' sym (FunTy ty1 ty2) = FunTy (opt_co sym ty1) (opt_co sym ty2)
+opt_co' sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co sym) tys))
+opt_co' sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co sym ty))
+
+opt_co' sym co@(TyVarTy tv)
+ | not (isCoVar tv) = co -- Identity; does not mention a CoVar
+ | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
+ | not sym = co
+ | otherwise = mkSymCoercion co
+ where
+ (ty1,ty2) = coVarKind tv
+
+opt_co' sym (ForAllTy tv cor)
+ | isCoVar tv = mkCoPredTy (opt_co sym co1) (opt_co sym co2) (opt_co sym cor)
+ | otherwise = ForAllTy tv (opt_co sym cor)
+ where
+ (co1,co2) = coVarKind tv
+
+opt_co' sym (TyConApp tc cos)
+ | isCoercionTyCon tc
+ = foldl mkAppTy opt_co_tc
+ (map (opt_co sym) (drop arity cos))
+ | otherwise
+ = TyConApp tc (map (opt_co sym) cos)
+ where
+ arity = tyConArity tc
+ opt_co_tc :: NormalCo
+ opt_co_tc = opt_co_tc_app sym tc (take arity cos)
+
+--------
+opt_co_tc_app :: Bool -> TyCon -> [Type] -> NormalCo
+-- Used for CoercionTyCons only
+opt_co_tc_app sym tc cos
+ | tc `hasKey` symCoercionTyConKey
+ = opt_co (not sym) co1
+
+ | tc `hasKey` transCoercionTyConKey
+ = if sym then opt_trans opt_co2 opt_co1
+ else opt_trans opt_co1 opt_co2
+
+ | tc `hasKey` leftCoercionTyConKey
+ , Just (co1, _) <- splitAppTy_maybe opt_co1
+ = co1
+
+ | tc `hasKey` rightCoercionTyConKey
+ , Just (_, co2) <- splitAppTy_maybe opt_co1
+ = co2
+
+ | tc `hasKey` csel1CoercionTyConKey
+ , Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
+ = s1
+
+ | tc `hasKey` csel2CoercionTyConKey
+ , Just (_,s2,_) <- splitCoPredTy_maybe opt_co1
+ = s2
+
+ | tc `hasKey` cselRCoercionTyConKey
+ , Just (_,_,r) <- splitCoPredTy_maybe opt_co1
+ = r
+
+ | tc `hasKey` instCoercionTyConKey
+ , Just (tv, co'') <- splitForAllTy_maybe opt_co1
+ , let ty = co2
+ = substTyWith [tv] [ty] co''
+
+ | otherwise -- 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) !!
+ = if sym then mkSymCoercion the_co
+ else the_co
+ where
+ the_co = TyConApp tc cos
+ (co1 : cos1) = cos
+ (co2 : _) = cos1
+ opt_co1 = opt_co sym co1
+ opt_co2 = opt_co sym co2
+
+-------------
+opt_trans :: NormalCo -> NormalCo -> NormalCo
+opt_trans co1 co2
+ | isIdNormCo co1 = co2
+ | otherwise = opt_trans1 co1 co2
+
+opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+-- First arg is not the identity
+opt_trans1 co1 co2
+ | isIdNormCo co2 = co1
+ | otherwise = opt_trans2 co1 co2
+
+opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+-- Neither arg is the identity
+opt_trans2 (TyConApp tc [co1a,co1b]) co2
+ | tc `hasKey` transCoercionTyConKey
+ = opt_trans1 co1a (opt_trans2 co1b co2)
+
+opt_trans2 co1 co2
+ | Just co <- opt_trans_rule co1 co2
+ = co
+
+opt_trans2 co1 (TyConApp tc [co2a,co2b])
+ | tc `hasKey` transCoercionTyConKey
+ , Just co1_2a <- opt_trans_rule co1 co2a
+ = if isIdNormCo co1_2a
+ then co2b
+ else opt_trans2 co1_2a co2b
+
+opt_trans2 co1 co2
+ = mkTransCoercion co1 co2
+
+------
+opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+opt_trans_rule (TyConApp tc [co1]) co2
+ | tc `hasKey` symCoercionTyConKey
+ , co1 `coreEqType` co2
+ , (_,ty2) <- coercionKind co2
+ = Just ty2
+
+opt_trans_rule co1 (TyConApp tc [co2])
+ | tc `hasKey` symCoercionTyConKey
+ , co1 `coreEqType` co2
+ , (ty1,_) <- coercionKind co1
+ = Just ty1
+
+opt_trans_rule (TyConApp tc1 [co1,ty1]) (TyConApp tc2 [co2,ty2])
+ | tc1 `hasKey` instCoercionTyConKey
+ , tc1 == tc2
+ , ty1 `coreEqType` ty2
+ = Just (mkInstCoercion (opt_trans2 co1 co2) ty1)
+
+opt_trans_rule (TyConApp tc1 cos1) (TyConApp tc2 cos2)
+ | not (isCoercionTyCon tc1) ||
+ getUnique tc1 `elem` [ leftCoercionTyConKey, rightCoercionTyConKey
+ , csel1CoercionTyConKey, csel2CoercionTyConKey
+ , cselRCoercionTyConKey ] --Yuk!
+ , tc1 == tc2 -- Works for left,right, and csel* family
+ -- BUT NOT equality axioms
+ -- E.g. (g Int) `trans` (g Bool)
+ -- /= g (Int . Bool)
+ = Just (TyConApp tc1 (zipWith opt_trans cos1 cos2))
+
+opt_trans_rule co1 co2
+ | Just (co1a, co1b) <- splitAppTy_maybe co1
+ , Just (co2a, co2b) <- splitAppTy_maybe co2
+ = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
+
+ | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
+ , Just (s2,t2,r2) <- splitCoPredTy_maybe co1
+ = Just (mkCoPredTy (opt_trans s1 s2)
+ (opt_trans t1 t2)
+ (opt_trans r1 r2))
+
+ | Just (tv1,r1) <- splitForAllTy_maybe co1
+ , Just (tv2,r2) <- splitForAllTy_maybe co2
+ , not (isCoVar tv1) -- Both have same kind
+ , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
+ = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
+
+opt_trans_rule _ _ = Nothing
+
+
+-------------
+isIdNormCo :: NormalCo -> Bool
+-- Cheap identity test: look for coercions with no coercion variables at all
+-- So it'll return False for (sym g `trans` g)
+isIdNormCo ty = go ty