Weird behaviour when passing a `List` as an implicit argument.

[purefunctor]

For a bit of context, I have the following source file:

data Proxy : (xs : List Type) -> Type where
  MkProxy : Proxy xs

mkProxy : {xs : List Type} -> Proxy xs
mkProxy = MkProxy

Steps to Reproduce

If we pass some list to mkProxy as such:

t : ?
t = mkProxy {xs = [Int, Nat, String, Char]}

Checking the type of t in the REPL/C-c C-t gives:

Proxy ?xs

However, if I call mkProxy on the REPL directly:

λΠ> :t mkProxy {xs = [Int, Nat, String, Char]}
mkProxy : Proxy [Int, Nat, String, Char]

Expected Behavior

t should resolve to whatever was passed, which in this case Proxy [Int, Nat, String, Char].

@gallais also mentioned that:

[...] It is very strange because even using

typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a

to get the normalised type in the REPL I still get Bar ?xs

Other Observations

This affects Vect too, and it seems to be rooted on Nil/(::) syntax:

data L : x -> Type where
  N : L x
  C : x -> L x -> L x

data Proxy : (xs : L Type) -> Type where
  MkProxy : Proxy xs

mkProxy : {xs : L Type} -> Proxy xs
mkProxy = MkProxy

pass : ?  -- Proxy (C Int (C Nat (C String N)))
pass = mkProxy {xs = (C Int (C Nat (C String N)))}

Nil : L x
Nil = N

(::) : x -> L x -> L x
(::) = C

fail : ?  -- Proxy ?xs
fail = mkProxy {xs = [Int, Nat, String]}

[gallais]

Interestingly, adding the ? to the body of t leads to a valid type being found:

t : ?
t = the ? $ mkProxy {xs = [Int, Nat, String, Char]}

λΠ> :t t
Main.t : Proxy [Int, Nat, String, Char]

[gallais]

This is very strange: the type I'm getting for xs does not make any sense to me.

LOG unelab.meta:50: Found meta (Main.{xs:373}) lookup returned Just ({_:0} : Int) -> ({_:0} : Int) -> Int))

[gallais]

Ok this is a fix. It's a bad idea because it's saving way too much stuff but at least it clarifies where the issue is: the definition for ?xs does not get serialised.

diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index e9c7994f..01ff5f60 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -284,7 +284,8 @@ writeToTTC extradata sourceFileName ttcFileName
     = do bin <- initBinary
          defs <- get Ctxt
          ust <- get UST
-         gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs
+         gdefs <- getSaveDefs (currentNS defs) !(allNames (gamma defs)) [] defs
          sourceHash <- hashFileWith defs.options.hashFn sourceFileName
          totalReq <- getDefaultTotalityOption
          log "ttc.write" 5 $ unwords

[gallais]

As always understanding part of the issue allows me to make things worse:

File MissingValue.idr

module MissingValue

data Proxy : (xs : List Nat) -> Type where
  MkProxy : Proxy xs

mkProxy : {xs : List Nat} -> Proxy xs
mkProxy = MkProxy

export
f : ?
f = mkProxy {xs = [1..5]}

export
size : Type -> Nat
size (Proxy ns) = sum ns
size _ = 0

export
typeOf : {a : Type} -> a -> Type
typeOf _ = a

File Main.idr

module Main

import MissingValue

main : IO ()
main = printLn $ size $ typeOf f

Running :exec main from a loaded Main.idr leads to a runtime error:

Exception: attempt to reference unbound identifier MissingValue-arg-376 at line 596, char 1028 of /PATH/build/exec/_tmpchez_app/_tmpchez.ss

?arg shows up when you look at the type of f in the buffer: MissingValue.f : Proxy [1 .. ?arg]