implicit arguments crash

[plredmond]

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1668179472_14471.hs

{-@
allLeq ::          n:Int ~> {x:[a] | len x == n} -> {y:[a] | len y == n} -> Bool @-}
allLeq :: Ord a =>             [a]               ->    [a]               -> Bool
allLeq [] [] = True
allLeq (x:xs) (y:ys) = x<=y && allLeq xs ys

Here is, I think, a valid use of implicit arguments. We constrain the input lists to be the same length, but don't specify that length explicitly. This causes a large "addC: malformed constraint:" error in my local checkout, and a somewhat smaller error of the same kind on the online demo (linked above).