Merge pull request #2236 from ucsd-progsys/fd/fix-anormalise

Fix A normalization when type binder and lets are mixed in the input

Author: facundominguez

liquid-prelude/liquid-prelude.cabal

@@ -25,7 +25,6 @@ library
                     Language.Haskell.Liquid.Equational
                     Language.Haskell.Liquid.Bag
                     Language.Haskell.Liquid.ProofCombinators
-                    KMeansHelper
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , ghc-prim

liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs

@@ -249,7 +249,21 @@ stitch γ e
        e'    <- normalize γ e
        bs    <- st_binds <$> get
        put bs'
-       return $ mkCoreLets bs e'
+       -- See Note [Shape of normalized terms]
+       let (tvs, e'') = collectTyBinders e'
+       return $ mkLams tvs (mkCoreLets bs e'')
+
+-- Note [Shape of normalized terms]
+--
+-- The termination checker in Termination.collectArguments expects the type
+-- binders to come before lets:
+--
+-- > \ (@a) -> let ... in \ b c d -> ...
+--
+-- Therefore, stitch makes sure to insert new lets after the type binders
+--
+-- > \ (@a) -> let lqanf... = ... in let ... in \ b c d -> ...
+--
 
 _mkCoreLets' :: [CoreBind] -> CoreExpr -> CoreExpr
 _mkCoreLets' bs e = mkCoreLets bs1 e1

liquid-prelude/src/KMeansHelper.hs tests/pos/KMeansHelper.hs

@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -ddump-ds #-}
+-- | Tests that liquid haskell can deal fine with HasCallStack.
+--
+-- See https://github.com/ucsd-progsys/liquidhaskell/issues/2235
+module T2235 where
+
+import Language.Haskell.Liquid.Prelude (liquidError)
+import GHC.Stack
+
+{-@ myhead :: {xs:[a] | len xs > 0} -> a @-}
+myhead :: HasCallStack => [a] -> a
+myhead (x:_) = x
+
+{-@ type PosInt = {v: Int | v > 0 } @-}
+{-@ type List a N = {v : [a] | (len v) = N} @-}
+{-@ type Matrix a Rows Cols  = (List (List a Cols) Rows) @-}
+{-@ transpose                :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}
+
+transpose                    :: Int -> Int -> [[a]] -> [[a]]
+transpose 0 _ _              = []
+transpose c r ((x:xs) : xss) = (x : map myhead xss) : transpose (c-1) r (xs : map tail xss)
+transpose c r ([] : _)       = liquidError "dead code"
+transpose c r []             = error "dead code"
+

tests/pos/T2235.hs

@@ -1614,6 +1614,7 @@ executable unit-pos-1
                     , T2091
                     , T2093
                     , T2096
+                    , T2235
                     , T385
                     , T531
                     , T595a
@@ -1901,6 +1902,7 @@ executable unit-pos-2
                     , Ite1
                     , Ite
                     , Jeff
+                    , KMeansHelper
                     , Keys
                     , Kmp
                     , KmpIO