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.
This issue is related e.g. to #319, #330 and others referring to interfaces and the use of dependent types.
Steps to Reproduce
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.