Issue with hints and search space: Can't find implementation

[wurmli]

This issue is related e.g. to #319, #330 and others referring to interfaces and the use of dependent types.

module QTTTrials

data Tbl : (n : Nat) -> Type where
  [noHints]
  Value : (k : Nat) -> (value : String) -> Tbl k

%hint
valueZero : Tbl 0
valueZero = Value 0 "zero"

%hint
valueOne : Tbl 1
valueOne = Value 1 "one"

showValue : {m : Nat} -> Tbl m => (m : Nat) -> String
showValue @{Value k value} k = value

Steps to Reproduce

QTTTrials> :r
1/1: Building QTTTrials (QTTTrials.idr)
Loaded file QTTTrials.idr
QTTTrials> showValue Z
(interactive):1:1--1:12:Can't find an implementation for Tbl ?m

Expected Behavior

I would expect that the unique values of type "Tbl 0" or "Tbl 1" are found.

Observed Behavior

The values are not found, and even though it seems that as a search space the family of types Tbl m is taken, the two values valueOne and valueTwo are missed.