address Orestis' comments

agda2hs.agda-lib

@@ -1,4 +1,4 @@
 name: agda2hs
 depend:
 include: lib
-flags: -W noUnsupportedIndexedMatch --erasure --no-projection-like
+flags: -W noUnsupportedIndexedMatch --erasure

src/Agda2Hs/AgdaUtils.hs

@@ -22,7 +22,6 @@ import Agda.TypeChecking.Monad ( topLevelModuleName )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Reduce ( reduceDefCopy )
-import Agda.TypeChecking.Records ( shouldBeProjectible )
 
 import Agda.Utils.Either ( isRight )
 import Agda.Utils.List ( initMaybe )

src/Agda2Hs/Compile/ClassInstance.hs

@@ -27,8 +27,7 @@ import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute ( Apply(applyE), absBody, absApp )
 import Agda.TypeChecking.Records
-import Agda.TypeChecking.Reduce ( reduce )
-import Agda.TypeChecking.Telescope (  mustBePi )
+import Agda.TypeChecking.Telescope ( mustBePi )
 
 import Agda.Utils.Lens
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )

src/Agda2Hs/Compile/Record.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE NamedFieldPuns #-}
 module Agda2Hs.Compile.Record where
 
 import Control.Monad ( unless, when )

src/Agda2Hs/Compile/Term.hs

@@ -1,7 +1,7 @@
 module Agda2Hs.Compile.Term where
 
 import Control.Arrow ( (>>>), (&&&) )
-import Control.Monad ( unless, msum )
+import Control.Monad ( unless )
 import Control.Monad.Reader
 
 import Data.Foldable ( toList )
@@ -23,7 +23,7 @@ import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records ( shouldBeProjectible )
 import Agda.TypeChecking.Datatypes ( getConType )
-import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, reduce )
+import Agda.TypeChecking.Reduce ( unfoldDefinitionStep )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM )
 import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
@@ -32,7 +32,6 @@ import Agda.Utils.Lens
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Monad
 import Agda.Utils.Size
-import Agda.Utils.Tuple ( mapSndM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
@@ -106,7 +105,7 @@ caseOf ty args = compileArgs ty args >>= \case
     let lam [] = id
         lam qs = Hs.Lambda () qs
     in return $ eApp (Hs.Case () e [Hs.Alt () p (Hs.UnGuardedRhs () $ lam ps b) Nothing]) es'
-  _ -> genericError "case_of_ must be fully applied to a lambda term."
+  _ -> genericError "case_of_ must be fully applied to a lambda term"
 
 
 -- | Compile @the@ to an explicitly-annotated Haskell expression.
@@ -119,8 +118,8 @@ expTypeSig _ _ = genericError "`the` must be fully applied"
 
 
 -- should really be named compileVar, TODO: rename compileVar
-compileV :: Int -> Type -> [Term] -> C (Hs.Exp ())
-compileV i ty es = do
+compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
+compileVar i ty es = do
   reportSDoc "agda2hs.compile.term" 10 $ text "Reached variable"
   name <- compileDBVar i
   compileApp (hsVar name) ty es
@@ -142,7 +141,7 @@ compileSpined ty tm =
 
     Var i es     -> Just $ do
       ty <- typeOfBV i
-      aux (compileV i ty) (Var i) ty es
+      aux (compileVar i ty) (Var i) ty es
 
     _            -> Nothing
   where
@@ -502,7 +501,6 @@ compileApp' acc ty args = acc <$> compileArgs ty args
 -- | Compile a list of arguments applied to a function of the given type.
 compileArgs :: Type -> [Term] -> C [Hs.Exp ()]
 compileArgs ty [] = pure []
--- TODO(flupe): use mustBePi
 compileArgs ty (x:xs) = do
   (a, b) <- mustBePi ty
   let rest = compileArgs (absApp b x) xs

src/Agda2Hs/Compile/Type.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeApplications, NamedFieldPuns #-}
+{-# LANGUAGE TypeApplications #-}
 
 -- | Compilation to Haskell types.
 module Agda2Hs.Compile.Type where

src/Agda2Hs/Compile/Types.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms, FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
 module Agda2Hs.Compile.Types where
 
 import Control.Applicative ( liftA2 )

src/Agda2Hs/Compile/Utils.hs

@@ -137,7 +137,7 @@ keepArg x = usableModality x && visible x
 keepClause :: Clause -> Bool
 keepClause = any keepArg . clauseType
 
-isPropSort :: Sort  -> C Bool
+isPropSort :: Sort -> C Bool
 isPropSort s = reduce s <&> \case
   Prop _ -> True
   _      -> False

test/UnboxPragma.agda

@@ -22,6 +22,7 @@ sort1 xs = xs [ looksfine ]
 sort2 : List Int → ∃ (List Int) IsSorted
 sort2 xs .el = xs
 sort2 xs .pf = looksfine
+
 {-# COMPILE AGDA2HS sort2 #-}
 
 sort3 : List Int → ∃ (List Int) IsSorted

test/golden/PartialCase.err

@@ -1,2 +1,2 @@
 test/Fail/PartialCase.agda:5,1-7
-case_of_ must be fully applied to a lambda term.
+case_of_ must be fully applied to a lambda term

test/golden/PartialCaseNoLambda.err

@@ -1,2 +1,2 @@
 test/Fail/PartialCaseNoLambda.agda:5,1-13
-case_of_ must be fully applied to a lambda term.
+case_of_ must be fully applied to a lambda term