remove dot pattern case, cleanup

src/Agda2Hs/Compile/Function.hs

@@ -299,21 +299,22 @@ checkInlinePragma :: Definition -> C ()
 checkInlinePragma def@Defn{defName = f} = do
   let Function{funClauses = cs} = theDef def
   case filter (isJust . clauseBody) cs of
-    [c] -> do
-      let Clause{clauseTel,namedClausePats = naps} = c
-      unlessM (allM (dget . dget <$> naps) allowedPat) $ genericDocError =<<
+    [c] ->
+      unlessM (allowedPats (namedClausePats c)) $ genericDocError =<<
         "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+>
-        "Inline functions can only use variable patterns, dot patterns, or transparent record constructor patterns."
+        "Inline functions can only use variable patterns or transparent record constructor patterns."
     _ ->
       genericDocError =<<
         "Cannot make function" <+> prettyTCM f <+> "inlinable." <+>
         "An inline function must have exactly one clause."
   where allowedPat :: DeBruijnPattern -> C Bool
         allowedPat VarP{} = pure True
-        allowedPat DotP{} = pure True
         -- only allow matching on (unboxed) record constructors
         allowedPat (ConP ch ci cargs) =
           isUnboxConstructor (conName ch) >>= \case
-            Just _  -> allM cargs (allowedPat . dget . dget)
+            Just _  -> allowedPats cargs
             Nothing -> pure False
         allowedPat _ = pure False
+
+        allowedPats :: NAPs -> C Bool
+        allowedPats pats = allM pats (allowedPat . dget . dget)

src/Agda2Hs/Compile/Term.hs

@@ -300,10 +300,7 @@ compileInlineFunctionApp :: QName -> Elims -> C (Hs.Exp ())
 compileInlineFunctionApp f es = do
   reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of inline function"
   Function { funClauses = cs } <- theDef <$> getConstInfo f
-  let [ Clause { namedClausePats = pats
-               , clauseBody = Just body
-               , clauseTel
-               } ] = filter (isJust . clauseBody) cs
+  let [ Clause { namedClausePats = pats } ] = filter (isJust . clauseBody) cs
   etaExpand (drop (length es) pats) es >>= compileTerm
   where
     -- inline functions can only have transparent constructor patterns and variable patterns

src/Agda2Hs/Compile/Type.hs

@@ -187,10 +187,7 @@ compileInlineType :: QName -> Elims -> C (Hs.Type ())
 compileInlineType f args = do
   Function { funClauses = cs } <- theDef <$> getConstInfo f
 
-  let [ Clause { namedClausePats = pats
-               , clauseBody = Just body
-               , clauseTel
-               } ] = filter (isJust . clauseBody) cs
+  let [ Clause { namedClausePats = pats } ] = filter (isJust . clauseBody) cs
 
   when (length args < length pats) $ genericDocError =<<
     text "Cannot compile inlinable type alias" <+> prettyTCM f <+> text "as it must be fully applied."
@@ -200,7 +197,7 @@ compileInlineType f args = do
 
   case r of
     YesReduction _ t -> compileType t
-    _                -> genericDocError =<< text "Could not reduce inline function" <+> prettyTCM f
+    _                -> genericDocError =<< text "Could not reduce inline type alias " <+> prettyTCM f
 
 compileDom :: ArgName -> Dom Type -> C CompiledDom
 compileDom x a

test/golden/Inline2.err

@@ -1,2 +1,2 @@
 test/Fail/Inline2.agda:5,1-6
-Cannot make function tail' inlinable. Inline functions can only use variable patterns, dot patterns, or transparent record constructor patterns.
+Cannot make function tail' inlinable. Inline functions can only use variable patterns or transparent record constructor patterns.