You can't create Dependent Pairs with List of Strings, Strings, or Ints, but Nats are OK

[Pytheas01]

Steps to Reproduce

a : (t : Type ** List t)
a = (String ** ["The answer is"])

b : (t : Type ** t)
b = (String ** "The answer is")

c : (t : Type ** List t)
c = (Integer ** [2])

d : (t : Type ** t)
d = (Integer ** 2)

e : (t : Type ** List t)
e = (Nat ** [2])

f : (t : Type ** t)
f = (Nat ** 2)

Expected Behavior

(String ** ["The answer is "]) : (t : Type ** List t)

(String ** "The answer is ") : (t : Type ** t)

(Integer ** [2]) : (t : Type ** List t)

(Integer ** 2) : (t : Type ** t)

Observed Behavior

   |
25 | a = (String ** ["The answer is"])
   |     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of a with expected type
        (t : Type ** List t)

When checking argument x to constructor Builtins.MkDPair:
        No such variable String

HListTests.idr:28:5-31:
   |
28 | b = (String ** "The answer is")
   |     ~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of b with expected type
        (t : Type ** t)

When checking argument x to constructor Builtins.MkDPair:
        No such variable String

HListTests.idr:31:5-20:
   |
31 | c = (Integer ** [2])
   |     ~~~~~~~~~~~~~~~~
When checking right hand side of c with expected type
        (t : Type ** List t)

When checking argument x to constructor Builtins.MkDPair:
        No such variable Integer

HListTests.idr:34:5-18:
   |
34 | d = (Integer ** 2)
   |     ~~~~~~~~~~~~~~
When checking right hand side of d with expected type
        (t : Type ** t)

When checking argument x to constructor Builtins.MkDPair:
        No such variable Integer

[Pytheas01]

Language : Idris 1.31 OS : MacOSX 10.14.4

[LeifW]

I've hit this myself often enough - it seems there's something screwy with the ** syntax, because just invoking the DPair constructor directly works:

a : (t : Type ** List t)
a = MkDPair String ["The answer is"]

You can use the DPair type constructor in the type signature, as well:

a : DPair Type (\t => List t)
a = MkDPair String ["The answer is"]