Non-dependent tactic argument fails to run tactic

[jespercockx]

Non-dependent tactic argument fails to run tactic

[andreasabel]

It seems we can get a cleaner implementation if we split out TacticAttribute from Attribute and then use Either Attribute TacticAttribute for the parsed attributes, which can then be handled after a partitionEithers by either applyAttr... or setTacticAttr.

agda/src/full/Agda/Syntax/Concrete/Attribute.hs

Lines 24 to 31 in 08b79a6

	-- | An attribute is a modifier for `ArgInfo`.
	data Attribute
	= RelevanceAttribute Relevance
	| QuantityAttribute Quantity
	| TacticAttribute (Ranged Expr)
	| CohesionAttribute Cohesion
	| LockAttribute Lock

TacticAttribute is in fact not a modifier of ArgInfo so it violates (see bedde3d, #3858) the dedication of Attribute given in its genesis (see 5f5efa7).

[jespercockx]

It seems like the macro just doesn't get called for fails.

[andreasabel]

@jespercockx Where in the code do we call these tactics? I failed to find it in Rules.Application or Rules.Term...

[andreasabel]

Oh, it is here:

agda/src/full/Agda/TypeChecking/Implicit.hs

Lines 107 to 125 in 08b79a6

	implicitNamedArgs n expand t0 = do
	t0' <- reduce t0
	reportSDoc "tc.term.args" 30 $ "implicitNamedArgs" <+> prettyTCM t0'
	reportSDoc "tc.term.args" 80 $ "implicitNamedArgs" <+> text (show t0')
	case unEl t0' of
	Pi dom@Dom{domInfo = info, domTactic = tac, unDom = a} b
	| let x = bareNameWithDefault "_" dom, expand (getHiding info) x -> do
	info' <- if hidden info then return info else do
	reportSDoc "tc.term.args.ifs" 15 $
	"inserting instance meta for type" <+> prettyTCM a
	reportSDoc "tc.term.args.ifs" 40 $ nest 2 $ vcat
	[ "x = " <+> text (show x)
	, "hiding = " <+> text (show $ getHiding info)
	]
	return $ makeInstance info
	(_, v) <- newMetaArg info' x CmpLeq a
	whenJust tac $ \ tac -> liftTCM $
	applyModalityToContext info $ unquoteTactic tac v a

[andreasabel]

Trace:

calling implicitNamedArgs
  sFun =  {_ : Set} → Set
  hx   =  Hidden
  mx   =  nothing
implicitNamedArgs {_ : Set} → Set
Checking named arg {_} : Set
implicitNamedArgs Set
checkApplication: checkHeadApplication returned
  v =  doTheThing
checkExpr doTheThing {_} : Set
  returns doTheThing

More detail:

implicitNamedArgs El 
  {_getSort = ..., unEl = Pi (Dom {domInfo = ArgInfo {...}}
  , domName = Nothing
  , domIsFinite = False
  , domTactic = Nothing
  , unDom = El {_getSort = ..., unEl = Sort (Univ UType (Max 0 []))}}) (NoAbs "_" El {_getSort = ..., unEl = Sort (Univ UType (Max 0 []))})}

Looks your tactic is dropped from the type of doTheThing : @(tactic auto) {Set} → Set and never makes it to the place of implicit argument insertion.

[andreasabel]

I would guess the tactic is already dropped in the parser, since applyAttr... ignores tactics, and there is a special setTacticAttr which is only called in certain places. This looks like bad engineering. Tactics should also be handled by applyAttr....

agda/src/full/Agda/Syntax/Parser/Parser.y

Lines 628 to 629 in 08b79a6

	| Attributes1 Application3 '->' Expr {% applyAttrs1 $1 (defaultArg $ rawApp $2) <&> \ dom ->
	Fun (getRange ($1,$2,$3,$4)) dom $4 }

[jespercockx]

@andreasabel Since work on this issue seems to have stalled, I am moving it to the later milestone. When the issue is resolved, please change it to the current milestone at the time of fixing.