I am trying to write a simple tuple type
open import Agda.Builtin.List
mutual
f : List Set -> Set
f T = g T T where
g : List Set -> List Set -> Set
g [] T = Tuple T
g (t ∷ rest) T = t -> g rest T
data Tuple (A : List Set) : Set where
MkTPL : f A
but agda-mode keeps giving me this error:
The target of a constructor must be the datatype applied to its
parameters, playground.g A A A isn't
when checking the constructor MkTPL in the declaration of Tuple
Clearly f A is a function type whose target is Tuple A
Is there any way to tell the compiler that the code is correct (atleast I believe it is)
Also, why does it say playground.g A A A, not playground.g A A?
The constructors of a data type must have a fixed, known number of arguments, so your approach is not going to work. See Data.Product.Nary.NonDependent
for a definition of heterogeneous tuples in the standard library.
Also, why does it say playground.g A A A, not playground.g A A?
That is because g
is defined in scope of T : List Set
, so it gets lambda-lifted to a function with three arguments of type List Set
. Compare your definition with:
f : List Set -> Set
f T = g T where
g : List Set -> Set
g [] = Tuple T
g (t ∷ rest) = t -> g rest
Now Agda reports playground.g A A
.