fix for issue #18, faulty defaulting inside instance decl

UU-ComputerScience · Feb 27, 2014 · aade7de · aade7de
1 parent b30abe9
commit aade7de
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 16 deletions.
diff --git a/EHC/src/ehc/EH/Infer.cag b/EHC/src/ehc/EH/Infer.cag
@@ -109,25 +109,17 @@ SEM Expr
                 decls       .   patTyVarMp          :=  @exTyVarMp1b
 
 %%[(9 hmtyinfer) hs
--- | split a list of predicates into non-ambiguous & ambiguous, using quantifications results tqoGam,
+-- | Construct a function which does quantification given some fixed environmental info
---   which (a.o.) administers which predicates could be merged for quantification, those not are then ambiguous
+mkDoValGamQuantify
-doPredAmbigSplit :: (x -> PredOcc) -> TQOGam -> [x] -> ([x],[x])
+  :: TyKiGam -> VarMp -> TyVarIdS -> ValGam
-doPredAmbigSplit get tqoGam prOccL
+     -> (Bool -> VarMp -> [PredOcc] -> (ValGam, VarMp, (VarMp, TQOGam)))
-  = partition (\o -> poPoi (get o) `Set.member` assumedByQuant) prOccL
+mkDoValGamQuantify valQuTyKiGam quTvKiVarMp noLetQuantTyVarIdS valGam_l_
-  where assumedByQuant = Set.unions $ map tmpoInsPrIdSet $ gamElts tqoGam
+  = \doQuant tyVarMp prOccL -> valGamQuantifyWithVarMp doQuant valQuTyKiGam quTvKiVarMp tyVarMp noLetQuantTyVarIdS prOccL valGam_l_
 %%]
 
 %%[(9 hmtyinfer)
 SEM Expr
-  | Let         loc         .   doValGamQuantify    =   \doQuant tyVarMp prOccL -> valGamQuantifyWithVarMp doQuant @valQuTyKiGam @quTvKiVarMp tyVarMp @noLetQuantTyVarIdS prOccL @valGam_l_
+  | Let         loc         .   doValGamQuantify    =   mkDoValGamQuantify @valQuTyKiGam @quTvKiVarMp @noLetQuantTyVarIdS @valGam_l_
-                            .   doPredAmbigSplitForSimplify
-                                                    =   \chrPrOccL
-                                                           -> let us                = mkNewLevUIDL (length chrPrOccL) uidStart
-                                                                  -- couple with arbitrary id's to make quantify & split work
-                                                                  prOccL            = zipWith (\u (o,_) -> cpo2PredOcc (mkPrId u) o) us chrPrOccL
-                                                                  (_,_, (_,tqoGam)) = @doValGamQuantify False @tyVarMpDeclsL01 prOccL
-                                                                  (namb,amb)        = doPredAmbigSplit fst tqoGam $ zip prOccL chrPrOccL
-                                                              in  (map snd amb, map snd namb)
                             .   (quValGam_qu_,quTyVarMp, (cycTyVarMp_l,tqoGam))
                                                     :=  @doValGamQuantify True @tyVarMpDeclsQuant @toQuantOverPrOccL
                             .   tmpoTyVarMp         =   foldr (\tmpo c -> tmpoImplsVarMp tmpo `varUpd` c) emptyVarMp (gamElts @tqoGam)
@@ -147,6 +139,47 @@ SEM Expr
                                                             @bodyVarMp2
                                                         `varUpd` @lhs.tyVarMp
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% Split for ambiguity check, required for defaulting
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%[(9 hmtyinfer) hs
+-- | split a list of predicates into non-ambiguous & ambiguous, using quantifications results tqoGam,
+--   which (a.o.) administers which predicates could be merged for quantification, those not are then ambiguous
+doPredAmbigSplit :: (x -> PredOcc) -> TQOGam -> [x] -> ([x],[x])
+doPredAmbigSplit get tqoGam prOccL
+  = partition (\o -> poPoi (get o) `Set.member` assumedByQuant) prOccL
+  where assumedByQuant = Set.unions $ map tmpoInsPrIdSet $ gamElts tqoGam
+
+-- | Split predicates according to whether the predicate combining part of quantification can be done
+mkDoPredAmbigSplitForSimplify :: (Bool -> vm -> [PredOcc] -> (dum1,dum2,(dum3,TQOGam))) -> vm -> [(CHRPredOcc, x)] -> ([(CHRPredOcc, x)],[(CHRPredOcc, x)])
+mkDoPredAmbigSplitForSimplify doValGamQuantify tyVarMpDeclsL01
+  = \chrPrOccL
+       -> let us                = mkNewLevUIDL (length chrPrOccL) uidStart
+              -- couple with arbitrary id's to make quantify & split work
+              prOccL            = zipWith (\u (o,_) -> cpo2PredOcc (mkPrId u) o) us chrPrOccL
+              (_,_, (_,tqoGam)) = doValGamQuantify False tyVarMpDeclsL01 prOccL
+              (namb,amb)        = doPredAmbigSplit fst tqoGam $ zip prOccL chrPrOccL
+          in  (map snd amb, map snd namb)
+%%]
+
+%%[(9 hmtyinfer)
+SEM Expr
+  | Let         loc         .   doPredAmbigSplitForSimplify
+                                                    =	mkDoPredAmbigSplitForSimplify @doValGamQuantify @tyVarMpDeclsL01
+%%]
+
+%%[(9 hmtyinfer)
+SEM Decl
+  | Instance    loc         .   doPredAmbigSplitForSimplify
+                                                    =	mkDoPredAmbigSplitForSimplify 
+                                                            (mkDoValGamQuantify
+                                                                @lhs.finTyKiGam @lhs.tvKiVarMp 
+                                                                (setSubst @tyVarMpDeclsL0 @decls.noLetQuantTyVarIdS)
+                                                                (gamTop @decls.patValGam))
+                                                            @tyVarMpDeclsL01
+%%]
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%% Restriction of @decls.tyVarMp to meta level 0
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

diff --git a/EHC/src/ehc/EH/ResolvePredCHR.cag b/EHC/src/ehc/EH/ResolvePredCHR.cag
@@ -510,7 +510,7 @@ SEM Decl
 %%]]
                                 )
                                                     =   ehcOptTrace @lhs.opts "Decl.Instance.simplify1" $ 
-                                                        simplify [SimplifyHow_Canonicalize] (@chrProveFIIn {fiUniq = @lUniq7}) @lhs.chrStore @lhs.clDfGam (heurScopedEHC @chrProveFIIn) ((,) []) Map.empty @toProveDeclsCnstrMp emptySimplifyResult
+                                                        simplify [SimplifyHow_Canonicalize] (@chrProveFIIn {fiUniq = @lUniq7}) @lhs.chrStore @lhs.clDfGam (heurScopedEHC @chrProveFIIn) @doPredAmbigSplitForSimplify Map.empty @toProveDeclsCnstrMp emptySimplifyResult
                             .   (chrSolveDeclsState,chrSolveDeclsRedGraph,chrSolveDeclsDoneConstraints,chrSolveDeclsTrace,_,_,_)
                                                     =   debugInfo @chrDeclsSimplifyResult
 

diff --git a/EHC/test/regress/99/Defaulting1.hs b/EHC/test/regress/99/Defaulting1.hs
@@ -0,0 +1,30 @@
+{- ----------------------------------------------------------------------------------------
+   what    : correct defaulting to Integer in instance decl, due to bug not doing so
+   expected: ok
+---------------------------------------------------------------------------------------- -}
+
+module Defaulting1 where
+
+f :: Num a => a -> ()
+f _ = ()
+
+class C a where
+  it :: a
+
+
+-- fix of previous bug:
+-- Here I get a type error:
+-- Test.hs:14-15:
+--   Predicates remain unproven:
+--     preds: UHC.Base.Num v_3_190_2
+--              at   : 
+--              trace: (UHC.Base.Num v_3_190_2,<4,0>,Test.hs:15:8): FAIL
+--                     (UHC.Base.Num v_3_190_2,<4,0>,Test.hs:15:8): FAIL
+instance C () where
+  it = f 0
+
+-- This one compiles fine.
+it' :: ()
+it' = f 0
+
+main = print (it :: ())