Hi. > Why don't we force people to be Honest instead of just being Good? No need to force people when you can force indices: https://hackage.haskell.org/package/Agda-2.5.2/docs/Agda-TypeChecking-Forcing.html With forcing some things are smaller than without it, see e.g. this issue: https://github.com/agda/agda/issues/1676