Thanks to a change by Atze, forward and backward reasoning (needed fo…

…r an example in the left-corner paper of Atze and Doaitse) now seems to work (although slow :( )

EHC/src/chr-experiment/Main.hs

@@ -12,25 +12,38 @@ import EH16.Pred.RedGraph
 import EH16.Base.Common
 import EH16.Pred.Heuristics
 import EH16.Pred.Evidence
+import EH16.VarMp
 import EH.Util.Pretty
 
 
 -- list of constraints
 input :: [Constraint CHRPredOcc RedHowAnnotation]
 input
-  = [ eq a tyA tyB
+  = {-[ eq a tyA tyB
     , eq a tyB tyC
     , eq a tyK1 ty1
     , eq p ty2 tyK1
+    ]-}
+    {-
+    [ eq a s1 tyC (mkProdApp [tyA, tyInt])
+    , eq a s2 tyC (mkProdApp [tyB, tyInt])
+    , eq p s3 tyA tyB
+    ]
+    -}
+    [ eq a s0 tyA tyB
+    , eq a s0 tyB tyC
+    -- , eq a s0 tyB tyA
+    , eq a s0 tyC tyB
+--    , eq p s0 tyInt tyInt
     ]
   where
-    a :: Pred -> Constraint CHRPredOcc RedHowAnnotation
-    a pr = Assume (mkCHRPredOcc pr initPredScope)
+    a :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation
+    a s pr = Assume (mkCHRPredOcc pr s)
 
-    p :: Pred -> Constraint CHRPredOcc RedHowAnnotation
-    p pr = Prove (mkCHRPredOcc pr initPredScope)
+    p :: PredScope -> Pred -> Constraint CHRPredOcc RedHowAnnotation
+    p s pr = Prove (mkCHRPredOcc pr s)
 
-    eq f t1 t2 = f (Pred_Eq t1 t2)
+    eq f s t1 t2 = f s (Pred_Eq t1 t2)
 
     [tyA, tyB, tyC, tyK1, tyK2, tyInt] = map (Ty_Con . HNm) ["A", "B", "C", "K1", "K2", "Int"]
     tyCI = Ty_Impls (Impls_Tail u1 []) `mk1Arrow` tyC
@@ -39,11 +52,17 @@ input
     ty2 = mkProdApp [tyK2 `mk1Arrow` tyCI, tyInt]
 
     [u1] = drop 7 (mkNewLevUIDL 8 uidStart)
+
+    s0 = PredScope_Lev []
+    s1 = PredScope_Lev [0]
+    s2 = PredScope_Lev [0,0]
+    s3 = PredScope_Lev [0,0,0]
 
 
 -- CHR rules
 store :: ScopedPredStore
-store
+store = initScopedPredStore
+{-
   = chrStoreFromElems
   $ [ -- symmetry (prove)
       [Prove eqT1T2] ==> [Prove eqT2T1, Reduction eqT1T2 RedHow_ByEqSymmetry [eqT2T1]]
@@ -59,7 +78,7 @@ store
                      |> [IsCtxNilReduction ty2 ty3]
     , -- congruence (results in new proof obligations, discarding the old by the congruence reduction)
       [Prove eqT1T2] ==> [Prove psPred, Reduction eqT1T2 RedHow_ByEqCongr [psPred]]
-                     |> [AreOblsByCongruence ty1 ty2 ps]
+                     |> [EqsByCongruence ty1 ty2 ps]
     , -- unpack predseq (cons)
       [Prove psCons] ==> [Prove psHead, Prove psPred, Reduction psCons RedHow_ByPredSeqUnpack [psHead, psPred]]
     , -- unpack predsec (nil)
@@ -81,13 +100,22 @@ store
     ps = PredSeq_Var u5
     pr = Pred_Var u6
     [u1,u2,u3,u4,u5,u6] = mkNewLevUIDL 6 uidStart
+-}
 
 
 env :: FIIn
 env = emptyFI { fiUniq = last $ mkNewLevUIDL 7 uidStart }
 
 producedCnstrs :: [Constraint CHRPredOcc RedHowAnnotation]
-producedCnstrs = chrSolve env store input
+tr :: SolveTrace CHRPredOcc RedHowAnnotation Guard VarMp
+(producedCnstrs,_,tr) = chrSolve' env store input
+
+steps :: PP_Doc
+steps = vlist tr
+
+dump :: IO ()
+dump = do writeFile "output.txt" (show steps)
+          putStrLn "dumped to output.txt"
 
 assumeMap :: CHRPredOccCnstrMp
 assumeMap = cnstrMpFromList [ (c, RedHow_Assumption (VarUIDHs_UID uidNull) (PredScope_Var uidNull)) | c <- producedCnstrs ]

EHC/src/ehc/CHR/Solve.chs

@@ -137,7 +137,8 @@ ppCHRStore' = ppCurlysCommasBlock . map (\(k,v) -> ppTrieKey k >-< indent 2 (":"
 
 %%[9
 type WorkKey = CHRKey
-type WorkUsedInMap = Map.Map CHRKey (Set.Set UsedByKey)
+-- type WorkUsedInMap = Map.Map CHRKey (Set.Set UsedByKey)
+type WorkUsedInMap = Map.Map (Set.Set CHRKey) (Set.Set UsedByKey)
 
 data Work p i
   = Work
@@ -298,12 +299,18 @@ chrSolve'' env chrStore cnstrs prevState
               (_:_)
                 -> expandMatch st matches
                 where expandMatch st@(SolveState {stWorkList = wl})
-                                  (((schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(CHR {chrBody = b, chrSimpSz = simpSz})}),(keys,works)),subst) : tlMatch)
+                                  ( ( ( schr@(StoredCHR {storedIdent = chrId, storedChr = chr@(CHR {chrBody = b, chrSimpSz = simpSz})})
+                                      , (keys,works)
+                                      )
+                                    , subst
+                                    ) : tlMatch
+                                  )
                         = expandMatch (st')
                           $ filter (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || isUsedByPropPart (wlUsedIn wl') r))
                           $ tlMatch
                         where (keysSimp,keysProp) = splitAt simpSz keys
-                              usedIn              = Map.fromListWith Set.union $ zip keysProp (repeat $ Set.singleton chrId)
+                              usedIn              = Map.singleton (Set.fromList keysProp) (Set.singleton chrId)
+                              -- usedIn              = Map.fromListWith Set.union $ zip keysProp (repeat $ Set.singleton chrId)
                               (bTodo,bDone)       = splitDone $ map (chrAppSubst subst) b
                               wl' = wlInsert bTodo
                                     $ wlDeleteByKey keysSimp
@@ -322,8 +329,8 @@ chrSolve'' env chrStore cnstrs prevState
                                          >-< "workkeys" >#< ppBracketsCommas (map ppTrieKey keys)
                                          >-< "worktrie" >#< wlTrie wl
                                          >-< "schr" >#< schr
-                                         >-< "usedin" >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl)
-                                         >-< "usedin'" >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl')
+                                         >-< "usedin" -- >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl)
+                                         >-< "usedin'" -- >#< (ppBracketsCommasV $ map (\(k,s) -> ppTrieKey k >#< ppBracketsCommas (map ppUsedByKey $ Set.toList s)) $ Map.toList $ wlUsedIn wl')
 %%][100
 %%]]
                       expandMatch st _ 
@@ -380,12 +387,16 @@ chrSolve'' env chrStore cnstrs prevState
                         cmb (Just s) next = fmap (`chrAppSubst` s) $ next s
                         cmb _        _    = Nothing
         isUsedByPropPart wlUsedIn (chr,(keys,_))
-          = all fnd $ drop (storedSimpSz chr) keys
-          where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup k wlUsedIn
+          = fnd $ drop (storedSimpSz chr) keys
+          where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup (Set.fromList k) wlUsedIn
         initState st = st { stWorkList = wlInsert wlnew $ stWorkList st, stDoneCnstrSet = Set.unions [Set.fromList done, stDoneCnstrSet st] }
                      where (wlnew,done) = splitDone cnstrs
         splitDone  = partition (\x -> cnstrRequiresSolve x)
 %%]
+        isUsedByPropPart wlUsedIn (chr,(keys,_))
+          = all fnd $ drop (storedSimpSz chr) keys
+          where fnd k = maybe False (storedIdent chr `Set.member`) $ Map.lookup k wlUsedIn
+
                 -> iter {- $ trp "YY" ("chr" >#< schr >-< ppwork) $ -} st'
                 r4 = foldr first Nothing $ r3
                 -- r5 = foldr first Nothing r4

EHC/src/ehc/Pred/CHR.chs

@@ -104,7 +104,7 @@ instance CHRSubstitutable Guard TyVarId VarMp where
 %%]]
 %%[[16
   chrFtv        (IsCtxNilReduction t1 t2)         = Set.unions [ftvSet t1, ftvSet t2]
-  chrFtv        (AreOblsByCongruence t1 t2 ps)    = Set.unions [ftvSet t1, ftvSet t2, ftvSet ps]
+  chrFtv        (EqsByCongruence t1 t2 ps)        = Set.unions [ftvSet t1, ftvSet t2, ftvSet ps]
 %%]]
 
   chrAppSubst s (HasStrictCommonScope   p1 p2 p3) = HasStrictCommonScope   (s |=> p1) (s |=> p2) (s |=> p3)
@@ -117,7 +117,7 @@ instance CHRSubstitutable Guard TyVarId VarMp where
 %%]]
 %%[[16
   chrAppSubst s (IsCtxNilReduction t1 t2)         = IsCtxNilReduction (s |=> t1) (s |=> t2)
-  chrAppSubst s (AreOblsByCongruence t1 t2 ps)    = AreOblsByCongruence (s |=> t1) (s |=> t2) (s |=> ps)
+  chrAppSubst s (EqsByCongruence t1 t2 ps)        = EqsByCongruence (s |=> t1) (s |=> t2) (s |=> ps)
   chrAppSubst s (UnequalTy t1 t2)                 = UnequalTy (s |=> t1) (s |=> t2)
 %%]]
 %%]
@@ -239,7 +239,7 @@ data Guard
 %%]]
 %%[[16
   | IsCtxNilReduction Ty Ty
-  | AreOblsByCongruence Ty Ty PredSeq
+  | EqsByCongruence Ty Ty PredSeq
   | UnequalTy Ty Ty
 %%]]
 %%]
@@ -256,7 +256,7 @@ ppGuard (NonEmptyRowLacksLabel  r o t l    ) = ppParens (t >#< "==" >#< ppParens
 %%]]
 %%[[16
 ppGuard (IsCtxNilReduction t1 t2           ) = t1 >#< "~>" >#< t2
-ppGuard (AreOblsByCongruence t1 t2 ps      ) = t1 >#< "~~" >#< t2 >#< "~>" >#< ps
+ppGuard (EqsByCongruence t1 t2 ps          ) = t1 >#< "~~" >#< t2 >#< "~>" >#< ps
 ppGuard (UnequalTy t1 t2                   ) = t1 >#< "/=" >#< t2
 %%]]
 %%]
@@ -337,7 +337,7 @@ instance CHRCheckable FIIn Guard VarMp where
               varMp = foVarMp fo
               tRes = varMp |=> foTy fo -- hum, I would assume that this substitution is already applied by fitsIn...?!
 
-          chk (AreOblsByCongruence t1 t2 obls)
+          chk (EqsByCongruence t1 t2 obls)
             = if foHasErrs fo || null preds
               then Nothing
               else return varMp
@@ -392,7 +392,7 @@ instance ForceEval Guard where
   forceEval x@(EqualScope             sc1 sc2    ) | forceEval sc1 `seq` forceEval sc2 `seq` True = x
   forceEval x@(NonEmptyRowLacksLabel  r o t l    ) | forceEval r `seq` forceEval o `seq` forceEval t `seq` forceEval l `seq` True = x
   forceEval x@(IsCtxNilReduction      t1 t2      ) | forceEval t1 `seq` forceEval t2 `seq` True = x
-  forceEval x@(AreOblsByCongruence    t1 t2 ps   ) | forceEval t1 `seq` forceEval t2 `seq` forceEval ps `seq` True = x
+  forceEval x@(EqsByCongruence    t1 t2 ps   ) | forceEval t1 `seq` forceEval t2 `seq` forceEval ps `seq` True = x
 %%[[101
   fevCount (HasStrictCommonScope   sc1 sc2 sc3) = cm1 "HasStrictCommonScope"  `cmUnion` fevCount sc1 `cmUnion` fevCount sc2 `cmUnion` fevCount sc3
   fevCount (IsStrictParentScope    sc1 sc2 sc3) = cm1 "IsStrictParentScope"   `cmUnion` fevCount sc1 `cmUnion` fevCount sc2 `cmUnion` fevCount sc3
@@ -401,7 +401,7 @@ instance ForceEval Guard where
   fevCount (EqualScope             sc1 sc2    ) = cm1 "EqualScope"            `cmUnion` fevCount sc1 `cmUnion` fevCount sc2
   fevCount (NonEmptyRowLacksLabel  r o t l    ) = cm1 "NonEmptyRowLacksLabel" `cmUnion` fevCount r   `cmUnion` fevCount o `cmUnion` fevCount t `cmUnion` fevCount l
   fevCount (IsCtxNilReduction      t1 t2      ) = cm1 "IsCtxNilReduction" `cmUnion` fevCount t1 `cmUnion` fevCount t2
-  fevCount (AreOblsByCongruence    t1 t2 ps   ) = cm1 "AreOblByCongruence" `cmUnion` fevCount t1 `cmUnion` fevCount t2 `cmUnion` fevCount ps
+  fevCount (EqsByCongruence        t1 t2 ps   ) = cm1 "EqsByCongruence" `cmUnion` fevCount t1 `cmUnion` fevCount t2 `cmUnion` fevCount ps
 %%]]
 %%]
 

EHC/src/ehc/Pred/CommonCHR.chs

@@ -50,6 +50,7 @@ data RedHowAnnotation
   |  RedHow_ByEqCongr
   |  RedHow_ByEqTyReduction !Ty !Ty
   |  RedHow_ByPredSeqUnpack
+  |  RedHow_ByEqFromAssume
 %%]]
   deriving (Eq, Ord)
 %%]
@@ -78,6 +79,7 @@ instance PP RedHowAnnotation where
   pp (RedHow_ByEqCongr   ) = pp "eqcongr"
   pp (RedHow_ByEqTyReduction ty1 ty2) = "eqtyred" >#< ty1 >#< "~>" >#< ty2
   pp (RedHow_ByPredSeqUnpack) = pp "unpack"
+  pp (RedHow_ByEqFromAssume)  = pp "eqassume"
 %%]]
 %%]
   pp (RedHow_ByInstance   s p sc)  =    "inst"   >#< s >|< sc >#< "::" >#< p
@@ -160,6 +162,7 @@ instance ForceEval RedHowAnnotation where
   fevCount (RedHow_ByEqCongr          )  = cm1 "RedHow_ByEqCongr"
   fevCount (RedHow_ByEqTyReduction ty1 ty2)  = cm1 "RedHow_ByEqTyReduction" `cmUnion` fevCount ty1 `cmUnion` fevCount ty2
   fevCount (RedHow_ByPredSeqUnpack    )  = cm1 "RedHow_ByPredSeqUnpack"
+  fevCount (RedHow_ByEqFromAssume     )  = cm1 "RedHow_ByEqFromAssume"
   fevCount (RedHow_ByLabel      l o sc)  = cm1 "RedHow_ByLabel"         `cmUnion` fevCount l `cmUnion` fevCount o `cmUnion` fevCount sc
   fevCount (RedHow_Lambda       i   sc)  = cm1 "RedHow_Lambda"      	`cmUnion` fevCount i `cmUnion` fevCount sc
 %%]]

EHC/src/ehc/Pred/EvidenceToCore.chs

@@ -138,7 +138,7 @@ evidMpToCore env evidMp
 %%]]
 %%[[16
         ignore (_, (Evid_Proof _ red  _))
-          | red `elem` [RedHow_ByEqSymmetry, RedHow_ByEqTrans, RedHow_ByEqCongr, RedHow_ByPredSeqUnpack]
+          | red `elem` [RedHow_ByEqSymmetry, RedHow_ByEqTrans, RedHow_ByEqCongr, RedHow_ByPredSeqUnpack, RedHow_ByEqFromAssume]
           = True
         ignore (_, (Evid_Proof _ (RedHow_ByEqTyReduction _ _) _))
           = True

EHC/src/ehc/Pred/Heuristics.chs

@@ -270,6 +270,8 @@ anncmpEHCScoped env ann1 ann2
 
 cmpEqReds :: RedHowAnnotation -> RedHowAnnotation -> PartialOrdering
 %%[[16
+cmpEqReds RedHow_ByEqFromAssume _        = P_GT
+cmpEqReds _ RedHow_ByEqFromAssume        = P_LT
 cmpEqReds (RedHow_Assumption _ _) _      = P_GT
 cmpEqReds _ (RedHow_Assumption _ _)      = P_LT
 cmpEqReds RedHow_ByPredSeqUnpack _       = P_GT

EHC/src/ehc/Pred/ToCHR.chs

@@ -76,7 +76,7 @@ Hence we can safely use non-unique variables.
 ([sc1,sc2,sc3]
  ,[pr1,pr2,pr3]
 %%[[10
- ,[ty1,ty2,ty3]
+ ,[ty1,ty2,ty3,ty4]
  ,[lab1]
  ,[off1]
 %%]]
@@ -88,7 +88,7 @@ Hence we can safely use non-unique variables.
   = ( map PredScope_Var [u1,u2,u3]
     , map Pred_Var [u7,u8,u9]
 %%[[10
-    , map mkTyVar [u10,u11,u14]
+    , map mkTyVar [u10,u11,u14,u15]
     , map Label_Var [u12]
     , map LabelOffset_Var [u13]
 %%]]
@@ -100,7 +100,7 @@ Hence we can safely use non-unique variables.
 %%[[9
   where [u1,u2,u3,u4,u5,u6,u7,u8,u9] = mkNewLevUIDL 9 uidStart
 %%][10
-  where [u1,u2,u3,u4,u5,u6,u7,u8,u9,u10,u11,u12,u13,u14] = mkNewLevUIDL 14 uidStart
+  where [u1,u2,u3,u4,u5,u6,u7,u8,u9,u10,u11,u12,u13,u14,u15] = mkNewLevUIDL 15 uidStart
 %%]]
 %%]
 
@@ -123,7 +123,7 @@ initScopedPredStore
       ++ [ instForall, predArrow, predSeq1, predSeq2 ]
 %%]]
 %%[[16
-      ++ [ rlEqSym, rlEqTrans1, rlEqTrans2, rlEqCongr, rlCtxToNil, rlUnpackCons, rlUnpackNil ]
+      ++ [ rlEqScope, rlEqTrans, rlEqSym, rlEqCongr, rlUnpackCons, rlCtxToNil, rlEqSymPrv, rlEqTransPrv, rlEqCongrPrv, rlUnpackConsPrv, rlUnpackNilPrv, rlPrvByAssume ]
 %%]]
   where p1s1         = mkCHRPredOcc pr1 sc1
         p1s2         = mkCHRPredOcc pr1 sc2
@@ -168,28 +168,31 @@ initScopedPredStore
                          <==> []
 %%]]
 %%[[16
-        eqT1T2 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc1
-        eqT2T1 = mkCHRPredOcc (Pred_Eq ty2 ty1) sc1
-        eqT2T3 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc2
-        eqT3T2 = mkCHRPredOcc (Pred_Eq ty3 ty2) sc2
-        eqT1T3 = mkCHRPredOcc (Pred_Eq ty1 ty3) sc1
-        psPred = mkCHRPredOcc (Pred_Preds pa1)  sc1
-        psCons = mkCHRPredOcc (Pred_Preds (PredSeq_Cons pr1 pa1)) sc1
-        psNil  = mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc1
-        psHead = mkCHRPredOcc pr1 sc1
+        eqT1T2s1 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc1
+        eqT1T2s2 = mkCHRPredOcc (Pred_Eq ty1 ty2) sc2
+        eqT2T1s1 = mkCHRPredOcc (Pred_Eq ty2 ty1) sc1
+        eqT2T3s1 = mkCHRPredOcc (Pred_Eq ty2 ty3) sc1
+        eqT1T3s1 = mkCHRPredOcc (Pred_Eq ty1 ty3) sc1
+        eqT3T4s2 = mkCHRPredOcc (Pred_Eq ty3 ty4) sc2
+        psPreds1 = mkCHRPredOcc (Pred_Preds pa1)  sc1
+        psConss1 = mkCHRPredOcc (Pred_Preds (PredSeq_Cons pr1 pa1)) sc1
+        psNils1  = mkCHRPredOcc (Pred_Preds PredSeq_Nil) sc1
+        psHeads1 = mkCHRPredOcc pr1 sc1
+
+        rlEqScope    = [Assume eqT1T2s1, Prove eqT3T4s2] ==> [Assume eqT1T2s2] |> [IsVisibleInScope sc1 sc2] -- push equality assumption downwards
+        rlEqSym      = [Assume eqT1T2s1] ==> [Assume eqT2T1s1]                                               -- symmetry
+        rlEqTrans    = [Assume eqT1T2s1, Assume eqT2T3s1] ==> [Assume eqT1T3s1]                              -- transitivity
+        rlEqCongr    = [Assume eqT1T2s1] ==> [Assume psPreds1] |> [EqsByCongruence ty1 ty2 pa1]              -- congruence
+        rlUnpackCons = [Assume psConss1] ==> [Assume psHeads1, Assume psPreds1]                              -- unpack a list of assumptions
+
+        rlCtxToNil      = [Prove eqT1T2s1] ==> [Prove eqT1T3s1, Reduction eqT1T2s1 (RedHow_ByEqTyReduction ty2 ty3) [eqT1T3s1]] |> [IsCtxNilReduction ty2 ty3]
+        rlEqSymPrv      = [Prove eqT1T2s1] ==> [Prove eqT2T1s1, Reduction eqT1T2s1 RedHow_ByEqSymmetry [eqT2T1s1]] |> [UnequalTy ty1 ty2]
+        rlEqTransPrv    = [Prove eqT1T2s1, Assume eqT2T3s1] ==> [Prove eqT1T3s1, Reduction eqT1T2s1 RedHow_ByEqTrans [eqT1T3s1, eqT2T3s1]] |> [UnequalTy ty2 ty3]
+        rlEqCongrPrv    = [Prove eqT1T2s1] ==> [Prove psPreds1, Reduction eqT1T2s1 RedHow_ByEqCongr [psPreds1]] |> [EqsByCongruence ty1 ty2 pa1]
+        rlUnpackConsPrv = [Prove psConss1] ==> [Prove psHeads1, Prove psPreds1, Reduction psConss1 RedHow_ByPredSeqUnpack [psHeads1, psPreds1]]
+        rlUnpackNilPrv  = [Prove psNils1]  ==> [Reduction psNils1 RedHow_ByPredSeqUnpack []]
+        rlPrvByAssume   = [Prove eqT1T2s1, Assume eqT1T2s1] ==> [Reduction eqT1T2s1 RedHow_ByEqFromAssume []]  -- dirty hack: generated assumptions by chr are not added to the graph, so made a reduction instead
 
-        rlEqSym      = [Prove eqT1T2] ==> [Prove eqT2T1, Reduction eqT1T2 RedHow_ByEqSymmetry [eqT2T1]]
-                                      |> [UnequalTy ty1 ty2]
-        rlEqTrans1   = [Prove eqT1T2, Assume eqT2T3] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT2T3]]
-                                                      |> [UnequalTy ty2 ty3, IsVisibleInScope sc2 sc1]
-        rlEqTrans2   = [Prove eqT1T2, Assume eqT3T2] ==> [Prove eqT1T3, Reduction eqT1T2 RedHow_ByEqTrans [eqT1T3, eqT3T2]]
-                                                      |> [UnequalTy ty2 ty3, IsVisibleInScope sc2 sc1]
-        rlEqCongr    = [Prove eqT1T2] ==> [Prove psPred, Reduction eqT1T2 RedHow_ByEqCongr [psPred]]
-                                       |> [AreOblsByCongruence ty1 ty2 pa1]
-        rlCtxToNil   = [Prove eqT1T2] ==> [Prove eqT1T3, Reduction eqT1T2 (RedHow_ByEqTyReduction ty2 ty3) [eqT1T3]]
-                                       |> [IsCtxNilReduction ty2 ty3]
-        rlUnpackCons = [Prove psCons] ==> [Prove psHead, Prove psPred, Reduction psCons RedHow_ByPredSeqUnpack [psHead, psPred]]
-        rlUnpackNil  = [Prove psNil]  ==> [Reduction psNil RedHow_ByPredSeqUnpack []]
 %%]]
         -- inclSc       = ehcCfgCHRInclScope $ feEHCOpts $ fiEnv env
 %%]

EHC/test/regress/16/gadt4.eh

@@ -0,0 +1,27 @@
+let
+
+data Ref a env
+ = Zero               , env = (a, env')
+ | Succ (Ref a env')  , env = (x, env')
+
+in let
+
+data Equal a b
+  = Eq, a = b
+
+in let
+
+data Maybe a
+  = Nothing
+  | Just a
+
+in let
+
+match :: Ref a env -> Ref b env -> Maybe (Equal a b)
+match = \r1 -> \r2 ->
+  case (r1, r2) of
+    (Zero, Zero) -> Just Eq
+    (Succ x, Succ y) -> match x y
+    (_, _)       -> Nothing
+
+in 3