Fix various bugs with the type generation of the deriving mechanism

Class/MonadTC.agda

@@ -12,6 +12,8 @@ open import Reflection.Syntax
 
 open import Reflection.Debug
 
+open import Class.Show
+open import Class.DecEq
 open import Class.MonadReader
 open import Class.MonadError
 open import Class.Functor
@@ -135,13 +137,82 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
       where _ → error ("Not a record!" ∷ᵈ [])
     return $ con c args
 
+  isSolvedMeta : Term → M Bool
+  isSolvedMeta m@(meta x args) = do
+    r@(meta y _) ← reduce m
+      where _ → return true
+    return (x ≠ y)
+  isSolvedMeta _ = error ("Not a meta!" ∷ᵈ [])
+
+  hasUnsolvedMetas : Term → M Bool
+  hasUnsolvedMetas' : List (Arg Term) → M Bool
+  hasUnsolvedMetasCl : List Clause → M Bool
+  hasUnsolvedMetasTel : Telescope → M Bool
+
+  hasUnsolvedMetas (var x args) = hasUnsolvedMetas' args
+  hasUnsolvedMetas (con c args) = hasUnsolvedMetas' args
+  hasUnsolvedMetas (def f args) = hasUnsolvedMetas' args
+  hasUnsolvedMetas (lam v (abs _ t)) = hasUnsolvedMetas t
+  hasUnsolvedMetas (pat-lam cs args) = do
+    a ← hasUnsolvedMetasCl cs
+    b ← hasUnsolvedMetas' args
+    return (a ∨ b)
+  hasUnsolvedMetas (pi (arg _ a) (abs _ b)) = do
+    a ← hasUnsolvedMetas a
+    b ← hasUnsolvedMetas b
+    return (a ∨ b)
+  hasUnsolvedMetas (sort (set t)) = hasUnsolvedMetas t
+  hasUnsolvedMetas (sort (prop t)) = hasUnsolvedMetas t
+  hasUnsolvedMetas (sort unknown) = return true
+  hasUnsolvedMetas (sort _) = return false
+  hasUnsolvedMetas (lit l) = return false
+  hasUnsolvedMetas m@(meta x x₁) = not <$> isSolvedMeta m
+  hasUnsolvedMetas unknown = return false
+
+  hasUnsolvedMetas' [] = return false
+  hasUnsolvedMetas' ((arg _ x) ∷ l) = do
+    a ← hasUnsolvedMetas x
+    b ← hasUnsolvedMetas' l
+    return (a ∨ b)
+
+  hasUnsolvedMetasCl [] = return false
+  hasUnsolvedMetasCl (clause tel _ t ∷ cl) = do
+    a ← hasUnsolvedMetas t
+    b ← hasUnsolvedMetasTel tel
+    c ← hasUnsolvedMetasCl cl
+    return (a ∨ b ∨ c)
+  hasUnsolvedMetasCl (absurd-clause tel _ ∷ cl) = do
+    a ← hasUnsolvedMetasTel tel
+    b ← hasUnsolvedMetasCl cl
+    return (a ∨ b)
+
+  hasUnsolvedMetasTel [] = return false
+  hasUnsolvedMetasTel ((_ , arg _ x) ∷ tel) = do
+    a ← hasUnsolvedMetas x
+    b ← hasUnsolvedMetasTel tel
+    return (a ∨ b)
+
   -- this allows mutual recursion
   declareAndDefineFuns : List (Arg Name × Type × List Clause) → M ⊤
   declareAndDefineFuns ds = do
     traverse (λ (n , t , _) → declareDef n t) ds
     traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds
     return _
 
+  declareAndDefineFunsDebug : List (Arg Name × Type × List Clause) → M ⊤
+  declareAndDefineFunsDebug ds = do
+    traverse (λ (n , t , _) → declareDef n t) ds
+    traverse (λ where (arg _ n , _ , _) → do
+      b ← getType n >>= hasUnsolvedMetas
+      if b then error [ strErr $ show n ] else return tt) ds
+    traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds
+    traverse (λ where (arg _ n , _ , _) → do
+      d@(function cs) ← getDefinition n
+        where _ → error [ strErr "Weird bug" ]
+      b ← hasUnsolvedMetasCl cs
+      if b then error [ strErr $ show d ] else return tt) ds
+    return _
+
   declareAndDefineFun : Arg Name → Type → List Clause → M ⊤
   declareAndDefineFun n ty cls = declareAndDefineFuns [ (n , ty , cls) ]
 

Reflection/Debug.agda

@@ -33,6 +33,9 @@ instance
   IsErrorPart-Name : IsErrorPart Name
   IsErrorPart-Name .toErrorPart = ErrorPart.nameErr
 
+  IsErrorPart-Pattern : IsErrorPart Pattern
+  IsErrorPart-Pattern .toErrorPart = ErrorPart.pattErr
+
   IsErrorPart-Clause : IsErrorPart Clause
   IsErrorPart-Clause .toErrorPart c = ErrorPart.termErr (pat-lam [ c ] [])
 

Reflection/Utils.agda

@@ -251,3 +251,9 @@ updateField fs rexp fn fexp =
     else
       clause [] [ vArg (proj f) ] (f ∙⟦ rexp ⟧)
     ) []
+
+toTelescope : List (Abs (Arg Type)) → Telescope
+toTelescope = map (λ where (abs n x) → (n , x))
+
+fromTelescope : Telescope → List (Abs (Arg Type))
+fromTelescope = map (λ where (n , x) → (abs n x))

Reflection/Utils/TCI.agda

@@ -224,6 +224,9 @@ viewAndReduceTy ty = helper ty =<< (length ∘ proj₁ ∘ viewTy) <$> normalise
 getType' : Name → M TypeView
 getType' n = viewAndReduceTy =<< getType n
 
+getTypeDB : ℕ → M TypeView
+getTypeDB n = viewAndReduceTy =<< inferType (♯ n)
+
 getDataDef : Name → M DataDef
 getDataDef n = inDebugPath "getDataDef" do
   debugLog ("Find details for datatype: " ∷ᵈ n ∷ᵈ [])
@@ -268,11 +271,11 @@ isSort t = do
     where _ → return false
   return true
 
-isNArySort : ℕ → Term → M Bool
-isNArySort n t = do
+isNArySort : Term → M (Bool × ℕ)
+isNArySort t = do
   (tel , ty) ← viewAndReduceTy t
   b ← isSort ty
-  return (⌊ (length tel) ≟ n ⌋ ∧ b)
+  return (b , length tel)
 
 isDefT : Name → Term → M Bool
 isDefT n t = do
@@ -293,8 +296,13 @@ withSafeReset x = runAndReset $ do
       debugLog ("In term: " ∷ᵈ t ∷ᵈ [])
       error1 "Unsolved metavariables remaining in withSafeReset!"
 
--- apply a list of terms to a name, picking the correct constructor & visibility
+-- apply a list of terms to a name, picking the correct constructor of the term datatype & visibility
 applyWithVisibility : Name → List Term → M Term
 applyWithVisibility n l = do
   (argTys , _) ← getType' n
   nameConstr n (zipWith (λ where (abs _ (arg i _)) → arg i) argTys l)
+
+applyWithVisibilityDB : ℕ → List Term → M Term
+applyWithVisibilityDB n l = do
+  (argTys , _) ← getTypeDB n
+  return $ var n (zipWith (λ where (abs _ (arg i _)) → arg i) argTys l)

Tactic/Assumption.agda

@@ -21,15 +21,6 @@ open import Reflection.Utils.TCI
 instance
   _ = Functor-M
 
-solve : ⦃ TCOptions ⦄ → Term → Tactic
-solve t = initTac $ runSpeculative $ do
-  inj₁ goal ← reader TCEnv.goal
-    where _ → error1 "solve: Goal is not a term!"
-  metas ← findMetas <$> checkType t goal
-  if null metas
-    then (_, true)  <$> unify goal t
-    else (_, false) <$> error1 "Unsolved metavariables remaining!"
-
 assumption' : ITactic
 assumption' = inDebugPath "assumption" do
   c ← getContext

Tactic/ClauseBuilder.agda

@@ -18,6 +18,7 @@ open SortingAlgorithm ≤-decTotalOrder (mergeSort ≤-decTotalOrder) public
 open import Reflection.Utils
 open import Reflection.Utils.TCI
 
+open import Class.Show
 open import Class.DecEq
 open import Class.Functor
 open import Class.MonadError.Instances
@@ -34,6 +35,8 @@ private variable
   a b : Level
   A : Set a
 
+open import Data.String as S using (parens)
+
 record ClauseBuilder (M : Set → Set) : Set₁ where
   field
     Base : Set → Set
@@ -241,7 +244,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
 
   -- if the goal is of type (a : A) → B, return the type of the branch of pattern p and new context
   specializeType : SinglePattern → Type → M (Type × Telescope)
-  specializeType p@(t , arg i p') goalTy = markDontFail "specializeType" $ inDebugPath "specializeType" $ runAndReset do
+  specializeType p@(t , arg i p') goalTy = inDebugPath "specializeType" $ runAndReset do
     debugLog ("Goal type to specialize: " ∷ᵈ goalTy ∷ᵈ [])
     cls@((Clause.clause tel _ _) ∷ _) ← return $ clauseExprToClauses $ MatchExpr $
         (p , inj₂ (just unknown)) ∷
@@ -261,7 +264,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
     return (goalTy' , newCtx)
 
   ContextMonad-MonadTC : ContextMonad M
-  ContextMonad-MonadTC .introPatternM pat x = do
+  ContextMonad-MonadTC .introPatternM pat@(_ , arg _ p) x = do
     goalTy ← goalTy
     (newGoalTy , newContext) ← specializeType pat goalTy
     extendContext' newContext (runWithGoalTy newGoalTy x)

Tactic/Derive.agda

@@ -34,39 +34,56 @@ open import Relation.Nullary.Decidable
 open import Tactic.ClauseBuilder
 
 open import Class.DecEq
-open import Class.Monad
-open import Class.Traversable
 open import Class.Functor
+open import Class.Monad
 open import Class.MonadReader.Instances
 open import Class.MonadTC.Instances
+open import Class.Show
+open import Class.Traversable
 
 instance
   _ = ContextMonad-MonadTC
   _ = Functor-M
+  _ = Show-List
 
 open ClauseExprM
 
+-- generate the type of the `className dName` instance
 genClassType : ℕ → Name → Maybe Name → TC Type
 genClassType arity dName wName = do
   params ← getParamsAndIndices dName
-  adjParams ← adjustParams $ take (length params ∸ arity) params
+  let params' = L.map (λ where (abs x y) → abs x (hide y)) $ take (length params ∸ arity) params
+  sorts ← collectRelevantSorts params'
+  debugLog1 ("Generate required instances at indices: " S.++ show (L.map proj₁ sorts))
+  let adjustedDBs = L.zipWith (λ (i , tel) a → (i + a , tel)) sorts (upTo (length sorts))
+  adjustedDBs' ← extendContext' (toTelescope params) $ genSortInstanceWithCtx adjustedDBs
+  let adjParams = params' ++ adjustedDBs'
   debugLog1 "AdjustedParams: "
-  logTelescope (L.map ((λ where (abs s x) → just s , x) ∘ proj₁) adjParams)
-  ty ← applyWithVisibility dName (L.map ♯ (trueIndices adjParams))
-  return $ modifyClassType wName (L.map proj₁ adjParams , ty)
+  logTelescope (L.map ((λ where (abs s x) → just s , x)) adjParams)
+  ty ← applyWithVisibility dName (L.map (♯ ∘ (_+ length sorts)) (downFrom (length params)))
+  return $ modifyClassType wName (adjParams , ty)
   where
-    adjustParams : List (Abs (Arg Type)) → TC (List ((Abs (Arg Type)) × Bool))
-    adjustParams [] = return []
-    adjustParams (abs x (arg _ t) ∷ l) = do
-      a ← (if_then [ (abs "_" (iArg (className ∙⟦ ♯ 0 ⟧)) , false) ] else []) <$> isNArySort arity t
-      ps ← extendContext (x , hArg t) (adjustParams l)
-      let ps' = flip L.map ps λ where
-        (abs s (arg i t) , b) → (abs s (arg i (mapVars (_+ (if b then length a else 0)) t)) , b)
-      return (((abs x (hArg t) , true) ∷ a) ++ ps')
-
-    trueIndices : {A : Set} → List (A × Bool) → List ℕ
-    trueIndices [] = []
-    trueIndices (x ∷ l) = if proj₂ x then length l ∷ trueIndices l else trueIndices l
+    -- returns list of DB indices (at the end) and telescope of argument types
+    collectRelevantSorts : List (Abs (Arg Type)) → TC (List (ℕ × ℕ))
+    collectRelevantSorts [] = return []
+    collectRelevantSorts (abs x (arg _ t) ∷ l) = do
+      rec ← extendContext (x , hArg t) $ collectRelevantSorts l
+      (b , k) ← isNArySort t
+      return (if b then (length l , k) ∷ rec else rec)
+
+    genSortInstance : ℕ → ℕ → ℕ → TC Term
+    genSortInstance k 0 i       = do
+      res ← applyWithVisibilityDB (i + k) (L.map ♯ $ downFrom k)
+      return $ className ∙⟦ res ⟧
+    genSortInstance k (suc a) i = do
+      res ← extendContext ("" , hArg unknown) $ genSortInstance k a i
+      return $ pi (hArg unknown) $ abs "_" res
+
+    genSortInstanceWithCtx : List (ℕ × ℕ) → TC (List (Abs (Arg Term)))
+    genSortInstanceWithCtx [] = return []
+    genSortInstanceWithCtx ((i , k) ∷ xs) = do
+      x' ← (abs "_" ∘ iArg) <$> (genSortInstance k k i)
+      (x' ∷_) <$> (extendContext ("", hArg unknown) $ genSortInstanceWithCtx xs)
 
     modifyClassType : Maybe Name → TypeView → Type
     modifyClassType nothing  (tel , ty) = tyView (tel , className ∙⟦ ty ⟧)
@@ -115,7 +132,7 @@ module _ (arity : ℕ) (genCe : (Name → Maybe Name) → List SinglePattern →
 
   derive-Class : ⦃ TCOptions ⦄ → List (Name × Name) → UnquoteDecl
   derive-Class l = initUnquoteWithGoal (className ∙) $
-    declareAndDefineFuns =<< concat <$> traverse ⦃ Functor-List ⦄ helper l
+    declareAndDefineFuns =<< runAndReset (concat <$> traverse ⦃ Functor-List ⦄ helper l)
     where
       helper : Name × Name → TC (List (Arg Name × Type × List Clause))
       helper (a , b) = do hs ← genMutualHelpers a ; deriveMulti (a , b , hs)

Tactic/Derive/Show.agda

@@ -70,12 +70,15 @@ private
   open import Tactic.Derive.TestTypes
   import Data.Nat.Show
   open import Tactic.Defaults
+  open import Data.List.Relation.Binary.Pointwise.Base
 
   unquoteDecl Show-Bool Show-ℤ Show-List Show-Maybe Show-ℕ Show-Sign Show-⊤ = derive-Show ((quote Bool , Show-Bool) ∷ (quote ℤ , Show-ℤ) ∷ (quote List , Show-List) ∷ (quote Maybe , Show-Maybe) ∷ (quote ℕ , Show-ℕ) ∷ (quote Sign , Show-Sign) ∷ (quote ⊤ , Show-⊤) ∷ [])
 
   unquoteDecl Show-Fin = derive-Show [ (quote Fin , Show-Fin) ]
   unquoteDecl Show-Vec = derive-Show [ (quote Vec , Show-Vec) ]
 
+  unquoteDecl Show-Pointwise = derive-Show [ (quote Pointwise , Show-Pointwise) ]
+
   unquoteDecl Show-These = derive-Show [ (quote These , Show-These) ]
   unquoteDecl Show-⊎ = derive-Show [ (quote _⊎_ , Show-⊎) ]