Description
Agda version: v2.6.4 (from Hackage)
For context, I'm trying to reproduce some basics from Clocked Type Theory, in particular postulating a forcing tick that works for any clock.
{-# OPTIONS --guarded #-}
primitive primLockUniv : Set₁
postulate ⋄ : {κ₀ : primLockUniv} → κ₀I get the following type error,
funSort Set₁ primLockUniv is not a valid sort
when checking that the expression {κ₀ : primLockUniv} → κ₀ is a type
which is fair, since according to the docs on the sort system I'm not allowed to do that. But if I try to cheat and assume a clock as a variable,
variable κ₀ : primLockUniv
postulate ⋄ : κ₀
force : {P : primLockUniv → Set} → (∀ κ → (@tick t : κ) → (P κ)) → (∀ κ → P κ)
force f κ = f κ ⋄I get a more serious error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Constraints.hs:71:11 in Agda-2.6.4-CPwNw3CagtPFruYK76yMGr:Agda.TypeChecking.Constraints
Explicitly setting the implicit argument gives what I assume is a more reasonable error:
force : {P : primLockUniv → Set} → (∀ κ → (@tick t : κ) → (P κ)) → (∀ κ → P κ)
force f κ = f κ (⋄ {κ₀ = κ})The term ⋄, given as an argument to the guarded value
f κ : κ → P κ
can not be used as a @tick argument, since it does not mention any @tick variables.
when checking that the expression f κ (⋄ {κ₀ = κ}) has type P κ
Interestingly, as an aside, I can write down the type of ⋄ as long as I let Agda infer the missing sort:
⋄′ : {κ₀ : _} → κ₀
⋄′ = ⋄