Fix Mimer trying bad recursive calls (#7195)

* Mimer: use monadic pretty printing combinators

* Mimer: use setMetaOccursCheck instead of creating fresh meta

* add "mimer.trace" debug printing giving a readable trace of the search

* Mimer: remove goalEnv

* add ViewPatterns to default extensions

* Mimer: make sure recursive call components get fresh metas after use

* add a NoSubst newtype wrapper with a trivial Subst instance

* Mimer: take care to only generate terminating recursive calls

* Mimer: issue 7116 test case

* add haddock for NoSubst

.hlint.yaml

@@ -133,6 +133,7 @@
     - -XTypeFamilies
     - -XTypeOperators
     - -XTypeSynonymInstances
+    - -XViewPatterns
 
 # Add custom hints for this project
 - hint:

Agda.cabal

@@ -342,6 +342,7 @@ common language
       TypeFamilies
       TypeOperators
       TypeSynonymInstances
+      ViewPatterns
 
   other-extensions:
       CPP

src/full/Agda/TypeChecking/Substitute/Class.hs

@@ -3,6 +3,8 @@
 module Agda.TypeChecking.Substitute.Class where
 
 import Control.Arrow ((***), second)
+import Control.DeepSeq
+import GHC.Generics
 
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -109,6 +111,16 @@ instance Subst QName where
   type SubstArg QName = Term
   applySubst _ q = q
 
+-- | Wrapper for types that do not contain variables (so applying a substitution is the identity).
+--   Useful if you have a structure of types that support substitution mixed with types that don't
+--   and need to apply a substitution to the full structure.
+newtype NoSubst t a = NoSubst { unNoSubst :: a }
+  deriving (Generic, NFData, Functor)
+
+instance DeBruijn t => Subst (NoSubst t a) where
+  type SubstArg (NoSubst t a) = t
+  applySubst _ x = x
+
 ---------------------------------------------------------------------------
 -- * Explicit substitutions
 ---------------------------------------------------------------------------

test/interaction/Issue7116.agda

@@ -0,0 +1,21 @@
+module _ (A : Set) where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Sigma
+
+data Color : Set where
+  black : Color
+
+data Tree' : Color → Nat → Set where
+  nb : ∀ (a : A) {c} {n}
+     → Tree' c n
+     → Tree' black n
+     → Tree' black (suc n)
+
+test : ∀ (a : A) {n} (l : Tree' black (suc n)) → Σ _ λ c → Tree' c (suc n)
+test a (nb b l r) = {!!}   -- C-c C-a
+-- was: internal error
+-- should be: black , nb a r r
+
+-- An internal error has occurred. Please report this as a bug.
+-- Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/CompiledClause/Match.hs:87:73

test/interaction/Issue7116.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_autoOne ""

test/interaction/Issue7116.out

@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : Σ Color (λ c → Tree' c (suc n)) " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "black , nb a r r")
+((last . 1) . (agda2-goals-action '()))