Cache coercion roles in NthCo
[ghc.git] / testsuite / tests / pmcheck / should_compile / T11195.hs
1 {-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
2 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
3
4 module T11195 where
5
6 import TyCoRep
7 import Coercion
8 import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
9 import TcType ( exactTyCoVarsOfType )
10 import CoAxiom
11 import VarSet
12 import VarEnv
13 import Pair
14 import InstEnv
15
16 type NormalCo = Coercion
17 type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
18 type SymFlag = Bool
19 type ReprFlag = Bool
20
21 chooseRole :: ReprFlag -> Role -> Role
22 chooseRole = undefined
23
24 wrapRole :: ReprFlag -> Role -> Coercion -> Coercion
25 wrapRole = undefined
26
27 wrapSym :: SymFlag -> Coercion -> Coercion
28 wrapSym = undefined
29
30 optForAllCoBndr :: LiftingContext -> Bool
31 -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
32 optForAllCoBndr = undefined
33
34 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
35 opt_trans = undefined
36
37 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
38 -> Type -> Type -> Coercion
39 opt_univ = undefined
40
41 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role
42 -> Role -> Coercion -> NormalCo
43 opt_co3 = undefined
44
45 opt_co2 :: LiftingContext -> SymFlag -> Role -> Coercion -> NormalCo
46 opt_co2 = undefined
47
48 compatible_co :: Coercion -> Coercion -> Bool
49 compatible_co = undefined
50
51 etaTyConAppCo_maybe = undefined
52 etaAppCo_maybe = undefined
53 etaForAllCo_maybe = undefined
54
55 matchAxiom = undefined
56 checkAxInstCo = undefined
57 isAxiom_maybe = undefined
58 isCohLeft_maybe = undefined
59 isCohRight_maybe = undefined
60
61 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
62 opt_transList is = zipWith (opt_trans is)
63
64 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
65 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
66 | d1 == d2
67 , co1 `compatible_co` co2 = undefined
68
69 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
70 | d1 == d2
71 , co1 `compatible_co` co2 = undefined
72
73 -- Push transitivity inside instantiation
74 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
75 | ty1 `eqCoercion` ty2
76 , co1 `compatible_co` co2 = undefined
77
78 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
79 in_co2@(UnivCo p2 r2 _tyl2 tyr2)
80 | Just prov' <- opt_trans_prov p1 p2 = undefined
81 where
82 -- if the provenances are different, opt'ing will be very confusing
83 opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv
84 = Just UnsafeCoerceProv
85 opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
86 = Just $ PhantomProv $ opt_trans is kco1 kco2
87 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
88 = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
89 opt_trans_prov (PluginProv str1) (PluginProv str2)
90 | str1 == str2 = Just p1
91 opt_trans_prov _ _ = Nothing
92
93 -- Push transitivity down through matching top-level constructors.
94 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1)
95 in_co2@(TyConAppCo r2 tc2 cos2)
96 | tc1 == tc2 = undefined
97
98 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
99 = undefined
100
101 -- Eta rules
102 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
103 | Just cos2 <- etaTyConAppCo_maybe tc co2 = undefined
104
105 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
106 | Just cos1 <- etaTyConAppCo_maybe tc co1 = undefined
107
108 opt_trans_rule is co1@(AppCo co1a co1b) co2
109 | Just (co2a,co2b) <- etaAppCo_maybe co2 = undefined
110
111 opt_trans_rule is co1 co2@(AppCo co2a co2b)
112 | Just (co1a,co1b) <- etaAppCo_maybe co1 = undefined
113
114 -- Push transitivity inside forall
115 opt_trans_rule is co1 co2
116 | ForAllCo tv1 eta1 r1 <- co1
117 , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
118
119 | ForAllCo tv2 eta2 r2 <- co2
120 , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined
121
122 where
123 push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
124
125 -- Push transitivity inside axioms
126 opt_trans_rule is co1 co2
127 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
128 , True <- sym
129 , Just cos2 <- matchAxiom sym con ind co2
130 , let newAxInst = AxiomInstCo con ind
131 (opt_transList is (map mkSymCo cos2) cos1)
132 , Nothing <- checkAxInstCo newAxInst
133 = undefined
134
135 -- TrPushAxR
136 | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
137 , False <- sym
138 , Just cos2 <- matchAxiom sym con ind co2
139 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
140 , Nothing <- checkAxInstCo newAxInst
141 = undefined
142
143 -- TrPushSymAxL
144 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
145 , True <- sym
146 , Just cos1 <- matchAxiom (not sym) con ind co1
147 , let newAxInst = AxiomInstCo con ind
148 (opt_transList is cos2 (map mkSymCo cos1))
149 , Nothing <- checkAxInstCo newAxInst
150 = undefined
151
152 -- TrPushAxL
153 | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
154 , False <- sym
155 , Just cos1 <- matchAxiom (not sym) con ind co1
156 , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
157 , Nothing <- checkAxInstCo newAxInst
158 = undefined
159
160 -- TrPushAxSym/TrPushSymAx
161 | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
162 , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
163 , con1 == con2
164 , ind1 == ind2
165 , sym1 == not sym2
166 , let branch = coAxiomNthBranch con1 ind1
167 qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
168 lhs = coAxNthLHS con1 ind1
169 rhs = coAxBranchRHS branch
170 pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
171 , all (`elemVarSet` pivot_tvs) qtvs
172 = undefined
173 where
174 co1_is_axiom_maybe = isAxiom_maybe co1
175 co2_is_axiom_maybe = isAxiom_maybe co2
176 role = coercionRole co1 -- should be the same as coercionRole co2!
177
178 opt_trans_rule is co1 co2
179 | Just (lco, lh) <- isCohRight_maybe co1
180 , Just (rco, rh) <- isCohLeft_maybe co2
181 , (coercionType lh) `eqType` (coercionType rh)
182 = undefined
183
184 opt_trans_rule _ co1 co2 -- Identity rule
185 | (Pair ty1 _, r) <- coercionKindRole co1
186 , Pair _ ty2 <- coercionKind co2
187 , ty1 `eqType` ty2
188 = undefined
189
190 opt_trans_rule _ _ _ = Nothing