Skip to content

Commit 5bea115

Browse files
committed
leave wired reflected as assumed
1 parent 72bd65a commit 5bea115

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/Language/Haskell/Liquid/Bare.hs

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -463,11 +463,12 @@ getReflects = fmap val . S.toList . S.unions . fmap (names . snd) . M.toList
463463
------------------------------------------------------------------------------------------
464464
addReflSigs :: GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
465465
------------------------------------------------------------------------------------------
466-
addReflSigs refl sig = sig { gsRefSigs = reflSigs, gsAsmSigs = filter notReflected (gsAsmSigs sig) }
466+
addReflSigs refl sig = sig { gsRefSigs = reflSigs, gsAsmSigs = wreflSigs ++ filter notReflected (gsAsmSigs sig) }
467467
where
468-
reflSigs = [ (x, t) | (x, t, _) <- gsHAxioms refl ]
469-
reflected = fst <$> reflSigs
470-
notReflected xt = (fst xt) `notElem` reflected
468+
(wreflSigs, reflSigs) = L.partition ((`elem` gsWiredReft refl) . fst)
469+
[ (x, t) | (x, t, _) <- gsHAxioms refl ]
470+
reflected = fst <$> (wreflSigs ++ reflSigs)
471+
notReflected xt = fst xt `notElem` reflected
471472

472473
makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> M.HashMap Ghc.Var (Maybe Int)
473474
makeAutoInst env name spec = Misc.hashMapMapKeys (Bare.lookupGhcVar env name "Var") (Ms.autois spec)

0 commit comments

Comments
 (0)