search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Bound Check Error #82

Closed 5HT closed 7 years ago

5HT commented 7 years ago 
> let a : (n: nat) * list nat = (zero,nil) in a.1
Checking: a
EVAL: zero
> let a : (n: nat) * list nat = (zero,nil) in a.2
Checking: a
EVAL: nil
> let a : (n: nat) * list nat = (zero,nil) in a.3
cubical: cannot add token at Err (Pn 46 1 47)
CallStack (from HasCallStack):
  error, called at ./Exp/Layout.hs:201:20 in main:Exp.Layout
mortberg commented 7 years ago

This doesn't have to do with bounds. a.1 and a.2 are just the first and second projections of a Sigma type, so a.3 doesn't make sense and the error is spotted at parse time. Ideally we should be able to give better error messages than this, but I don't think we can do much as we are using BNFC to generate the parser. One could imagine adding .N (where N is a natural number) to the grammar and then print a better error message when one is resolving what has been parsed. However I don't think it's worth it to pollute the grammar this way just to be able to print an error message, so I'm closing this issue.