Annotate 'Lazy' with reason for laziness

i.e. is it just for evaluation, or is it for codata? This will be useful
for mixed induction/coinduction and allow the productivity checker to be
cleverer.