I'm getting a problem where I have a value with type fun a, with fun being a function and a a value which doesn't get computed at type-checking and throws an unification error when I force it to be the result of that function application.
The specific error is this:
When checking right hand side of testRec2 with expected type
Record [("A", String), ("C", Nat)]
Type mismatch between
Record (projectLeft ["A", "C"]
[("A", String),
("B", String),
("C", Nat)]) (Type of hProjectByLabels_comp ["A",
"C"]
testRec1
(getYes (isSet ["A",
"C"])))
and
Record [("A", String), ("C", Nat)] (Expected type)
Specifically:
Type mismatch between
projectLeft ["A", "C"]
[("A", String), ("B", String), ("C", Nat)]
and
[("A", String), ("C", Nat)]
This is from an implementation of HList-like records in Idris, with the following example:
testRec1 : Record [("A", String), ("B", String), ("C", Nat)]
-- testRec1's value is already defined
testRec2 : Record [("A", String), ("C", Nat)]
testRec2 = hProjectByLabels_comp ["A", "C"] testRec1 (getYes $ isSet ["A", "C"])
... the following types:
IsSet : List t -> Type
isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)
LabelList : Type -> Type
IsLabelSet : LabelList lty -> Type
HList : LabelList lty -> Type
Record : LabelList lty -> Type
recToHList : Record ts -> HList ts
recLblIsSet : Record ts -> IsLabelSet ts
hListToRec : DecEq lty => {ts : LabelList lty} -> {prf : IsLabelSet ts} -> HList ts -> Record ts
IsProjectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type
IsProjectRight : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type
hProjectByLabelsHList : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> HList ts -> ((ls1 : LabelList lty ** (HList ls1, IsProjectLeft ls ts ls1)), (ls2 : LabelList lty ** (HList ls2, IsProjectRight ls ts ls2)))
projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
hProjectByLabelsLeftIsSet_Lemma2 : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsLabelSet ts1 -> IsLabelSet ts2
fromIsProjectLeftToComp : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsSet ls -> ts2 = projectLeft ls ts1
hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)
... and the following (necessary) definitions:
LabelList : Type -> Type
LabelList lty = List (lty, Type)
IsLabelSet : LabelList lty -> Type
IsLabelSet ts = IsSet (map fst ts)
projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft [] ts = []
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
projectLeft ls ((l,ty) :: ts) | Yes lIsInLs =
let delLFromLs = deleteElem ls lIsInLs
rest = projectLeft delLFromLs ts
in (l,ty) :: rest
projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts
deleteElem : (xs : List t) -> Elem x xs -> List t
deleteElem (x :: xs) Here = xs
deleteElem (x :: xs) (There inThere) =
let rest = deleteElem xs inThere
in x :: rest
getYes : (d : Dec p) -> case d of { No _ => (); Yes _ => p}
getYes (No _ ) = ()
getYes (Yes prf) = prf
hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)
hProjectByLabels_comp {ts} ls rec lsIsSet =
let
isLabelSet = recLblIsSet rec
hs = recToHList rec
(lsRes ** (hsRes, prjLeftRes)) = fst $ hProjectByLabelsHList ls hs
isLabelSetRes = hProjectByLabelsLeftIsSet_Lemma2 prjLeftRes isLabelSet
resIsProjComp = fromIsProjectLeftToComp prjLeftRes lsIsSet
recRes = hListToRec {prf=isLabelSetRes} hsRes
in rewrite (sym resIsProjComp) in recRes
Basically, there is a function projectLeft that is applied to 2 lists and returns a new one. The type of hProjectByLabels_comp applies this function at the type-level.
To actually construct the resulting list, I have a predicate of the style Pred l1 l2 l3 and a lemma of the style Pred l1 l2 l3 -> l3 = projectLeft l1 l2. In hProjectByLabels_comp I apply the lemma to the predicate and use rewrite to get the correct type-signature (rewriting l3, which is implicit in the predicate that appears inside the implementation, into projectLeft l1 l2, or projectLeft ls ts in this specific case).
I would expect that applying hProjectByLabels_comp to a record will compute projectLeft ls ts correctly. However, in the example above it fails to evaluate/compute projectLeft ["A", "C"] [("A", String), ("B", String), ("C", Nat)]. This seems weird, since evaluating that function application in the REPL gives exactly [("A", String), ("C", Nat)], which is what the type expects, but Idris can't seem to compute this function when type-checking.
I am not sure if the implementation of some of the lemmas/functions has anything to do with this or if it's just something about the types alone.
I tried replicating this error using a simpler example (with predicates and functions on Nats) but that simpler example type-checked correctly, so I couldn't find another way to replicate this error.
I'm using Idris 0.9.20.2
Edit: I tried rewriting projectLeft in the following way to see if anything changed but it keeps showing the same error
projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
projectLeft ls ((l,ty) :: ts) | Yes lIsInLs =
let delLFromLs = deleteElem ls lIsInLs
rest = projectLeft delLFromLs ts
in (l,ty) :: rest
projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts
testRec1does not have any value assigned, is that intentional? Otherwise, you can't depend on the computational behaviour of something that has a hole inside. – Yet Another GeektestRec1already exists (it has no holes inside). – gonzaw