Unexpected type-checking behavior with let and DataKinds
When playing around with the code for known-length vectors from #19722, I noticed following behavior in the type-checker when trying to implement a function to get the last element of a vector.
last :: Vec (Succ n) a -> a last (x :> Nil) = x last (_ :> xs) = case xs of x' :> xs' -> last xs --last (_ :> xs) = let (x' :> xs') = xs in last xs --last (_ :> xs) = let (x' :> xs') = xs in last (x' :> xs')
The main issue here is that we can't just write
last (_ :> xs) = last xs, because then GHC can't verify that the type of
xs is really
Vec (Succ n) a.
So the workaround is to let GHC know that
xs is really non-empty in this second case.
The first version of the case
_ :> xs using a case-expression compiles fine, but the two version implemented using let-expressions don't type-check.
I lack an in-depth understanding of the type-checker or even the DataKinds extension, but I think the 3 versions are semantically identical.
Make all 3 versions type-check.