diff --git a/.travis.yml b/.travis.yml index dfdb55ba06..fda71c297f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -25,18 +25,18 @@ env: - GHC="7.8.4" CABAL="1.18" SMT=z3 TESTS=Benchmarks/icfp_pos - GHC="7.8.4" CABAL="1.18" SMT=z3 TESTS=Benchmarks/icfp_neg - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Unit/pos - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Unit/neg - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Unit/crash - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/text - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/bytestring - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/esop - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/vect-algs - # - GHC="7.10.1" CABAL="1.22" SMT=cvc4 TESTS=Unit/pos - # - GHC="7.10.1" CABAL="1.22" SMT=cvc4 TESTS=Unit/neg - # - GHC="7.10.1" CABAL="1.22" SMT=cvc4 TESTS=Unit/crash - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/icfp_pos - - GHC="7.10.1" CABAL="1.22" SMT=z3 TESTS=Benchmarks/icfp_neg + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Unit/pos + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Unit/neg + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Unit/crash + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/text + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/bytestring + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/esop + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/vect-algs + # - GHC="7.10.2" CABAL="1.22" SMT=cvc4 TESTS=Unit/pos + # - GHC="7.10.2" CABAL="1.22" SMT=cvc4 TESTS=Unit/neg + # - GHC="7.10.2" CABAL="1.22" SMT=cvc4 TESTS=Unit/crash + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/icfp_pos + - GHC="7.10.2" CABAL="1.22" SMT=z3 TESTS=Benchmarks/icfp_neg # ugh... Classify.hs is too slow and makes travis think the build is stalled # - TESTS=hscolour diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal index 556bc331e2..461e21aeb1 100644 --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -54,7 +54,7 @@ Flag include Executable liquid default-language: Haskell98 Build-Depends: base >= 4 && < 5 - , ghc>=7.8.3 + , ghc == 7.8.3 || == 7.8.4 || == 7.10.2 , ansi-terminal , template-haskell , time diff --git a/src/Language/Haskell/Liquid/Bare/Lookup.hs b/src/Language/Haskell/Liquid/Bare/Lookup.hs index 4834a7fd36..d0e5333f44 100644 --- a/src/Language/Haskell/Liquid/Bare/Lookup.hs +++ b/src/Language/Haskell/Liquid/Bare/Lookup.hs @@ -105,7 +105,7 @@ symbolLookupEnv env mod s res' <- lookupRdrName env modName (setRdrNameSpace rn tcName) return $ catMaybes [res, res'] | otherwise - = do L _ rn <- hscParseIdentifier env $ symbolString s + = do rn <- hscParseIdentifier env $ symbolString s (_, lookupres) <- tcRnLookupRdrName env rn case lookupres of Just ns -> return ns diff --git a/src/Language/Haskell/Liquid/Desugar710/DsBinds.hs b/src/Language/Haskell/Liquid/Desugar710/DsBinds.hs index 3b9b52a3b9..6c29a395ec 100644 --- a/src/Language/Haskell/Liquid/Desugar710/DsBinds.hs +++ b/src/Language/Haskell/Liquid/Desugar710/DsBinds.hs @@ -46,11 +46,12 @@ import TcEvidence import TcType import Type import Coercion hiding (substCo) -import TysWiredIn ( eqBoxDataCon, coercibleDataCon, tupleCon ) +import TysWiredIn ( eqBoxDataCon, coercibleDataCon, mkListTy + , mkBoxedTupleTy, stringTy, tupleCon ) import Id import MkId(proxyHashId) import Class -import DataCon ( dataConWorkId ) +import DataCon ( dataConWorkId, dataConTyCon ) import Name import MkId ( seqId ) import IdInfo ( IdDetails(..) ) @@ -908,6 +909,8 @@ dsEvTerm (EvLit l) = EvNum n -> mkIntegerExpr n EvStr s -> mkStringExprFS s +dsEvTerm (EvCallStack cs) = dsEvCallStack cs + dsEvTerm (EvTypeable ev) = dsEvTypeable ev dsEvTypeable :: EvTypeable -> DsM CoreExpr @@ -1025,6 +1028,62 @@ the proxy argument. This is what went wrong in #3245 and #9203. So we help GHC by manually keeping the 'rep' *outside* the lambda. -} + + +dsEvCallStack :: EvCallStack -> DsM CoreExpr +-- See Note [Overview of implicit CallStacks] in TcEvidence.hs +dsEvCallStack cs = do + df <- getDynFlags + m <- getModule + srcLocDataCon <- dsLookupDataCon srcLocDataConName + let srcLocTyCon = dataConTyCon srcLocDataCon + let srcLocTy = mkTyConTy srcLocTyCon + let mkSrcLoc l = + liftM (mkCoreConApps srcLocDataCon) + (sequence [ mkStringExprFS (packageKeyFS $ modulePackageKey m) + , mkStringExprFS (moduleNameFS $ moduleName m) + , mkStringExprFS (srcSpanFile l) + , return $ mkIntExprInt df (srcSpanStartLine l) + , return $ mkIntExprInt df (srcSpanStartCol l) + , return $ mkIntExprInt df (srcSpanEndLine l) + , return $ mkIntExprInt df (srcSpanEndCol l) + ]) + + let callSiteTy = mkBoxedTupleTy [stringTy, srcLocTy] + + matchId <- newSysLocalDs $ mkListTy callSiteTy + + callStackDataCon <- dsLookupDataCon callStackDataConName + let callStackTyCon = dataConTyCon callStackDataCon + let callStackTy = mkTyConTy callStackTyCon + let emptyCS = mkCoreConApps callStackDataCon [mkNilExpr callSiteTy] + let pushCS name loc rest = + mkWildCase rest callStackTy callStackTy + [( DataAlt callStackDataCon + , [matchId] + , mkCoreConApps callStackDataCon + [mkConsExpr callSiteTy + (mkCoreTup [name, loc]) + (Var matchId)] + )] + let mkPush name loc tm = do + nameExpr <- mkStringExprFS name + locExpr <- mkSrcLoc loc + case tm of + EvCallStack EvCsEmpty -> return (pushCS nameExpr locExpr emptyCS) + _ -> do tmExpr <- dsEvTerm tm + -- at this point tmExpr :: IP sym CallStack + -- but we need the actual CallStack to pass to pushCS, + -- so we use unwrapIP to strip the dictionary wrapper + -- See Note [Overview of implicit CallStacks] + let ip_co = unwrapIP (exprType tmExpr) + return (pushCS nameExpr locExpr (mkCastDs tmExpr ip_co)) + case cs of + EvCsTop name loc tm -> mkPush name loc tm + EvCsPushCall name loc tm -> mkPush (occNameFS $ getOccName name) loc tm + EvCsEmpty -> panic "Cannot have an empty CallStack" + + --------------------------------------- dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr -- This is the crucial function that moves diff --git a/src/Language/Haskell/Liquid/Desugar710/DsUtils.hs b/src/Language/Haskell/Liquid/Desugar710/DsUtils.hs index 2b036a1ca9..e8c730f9f5 100644 --- a/src/Language/Haskell/Liquid/Desugar710/DsUtils.hs +++ b/src/Language/Haskell/Liquid/Desugar710/DsUtils.hs @@ -24,7 +24,7 @@ module Language.Haskell.Liquid.Desugar710.DsUtils ( mkCoPrimCaseMatchResult, mkCoAlgCaseMatchResult, mkCoSynCaseMatchResult, wrapBind, wrapBinds, - mkErrorAppDs, mkCoreAppDs, mkCoreAppsDs, + mkErrorAppDs, mkCoreAppDs, mkCoreAppsDs, mkCastDs, seqVar, @@ -44,6 +44,7 @@ import {-# SOURCE #-} Language.Haskell.Liquid.Desugar710.Match ( matchSimply ) import HsSyn import TcHsSyn +import Coercion( Coercion, isReflCo ) import TcType( tcSplitTyConApp ) import CoreSyn import DsMonad @@ -549,6 +550,18 @@ mkCoreAppDs fun arg = mkCoreApp fun arg -- The rest is done in MkCore mkCoreAppsDs :: CoreExpr -> [CoreExpr] -> CoreExpr mkCoreAppsDs fun args = foldl mkCoreAppDs fun args +mkCastDs :: CoreExpr -> Coercion -> CoreExpr +-- We define a desugarer-specific verison of CoreUtils.mkCast, +-- because in the immediate output of the desugarer, we can have +-- apparently-mis-matched coercions: E.g. +-- let a = b +-- in (x :: a) |> (co :: b ~ Int) +-- Lint know about type-bindings for let and does not complain +-- So here we do not make the assertion checks that we make in +-- CoreUtils.mkCast; and we do less peephole optimisation too +mkCastDs e co | isReflCo co = e + | otherwise = Cast e co + {- ************************************************************************ * *