search

fmease / lushui

The reference compiler of the Lushui programming language
Apache License 2.0
7 stars 0 forks source link

We don't evaluate expressions during term equivalence check #32

Open fmease opened 4 years ago

fmease commented 4 years ago

Meta: Add description.

Example:

F: Type = F

;;; @Bug does not overflow because equals does not evaluate
x: F = Type

use extern.core.nat.(+ Nat)

f (n: Nat): Nat = + 1 (f n)

data Holder (n: Nat): Type of

;;; @Bug should overflow but does not
y: Holder (f 100000) = Type

Output: 

error[E032]: expected type `topmost.F` but got type `Type`
 --> /home/fmease/programming/main_projects/lushui/bugs/no-computation-during-type-checking.lushui:4:4
  |
4 | x: F = Type
  |    - expected due to this
  |
 --> /home/fmease/programming/main_projects/lushui/bugs/no-computation-during-type-checking.lushui:4:8
  |
4 | x: F = Type
  |        ^^^^ has the wrong type
  |

error[E032]: expected type `topmost.Holder (topmost.f 100000)` but got type `Type`
  --> /home/fmease/programming/main_projects/lushui/bugs/no-computation-during-type-checking.lushui:13:4
   |
13 | y: Holder (f 100000) = Type
   |    ----------------- expected due to this
   |
  --> /home/fmease/programming/main_projects/lushui/bugs/no-computation-during-type-checking.lushui:13:24
   |
13 | y: Holder (f 100000) = Type
   |                        ^^^^ has the wrong type
   |