Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compiling flat vector doesn't terminate #7

Open
eayus opened this issue Jan 4, 2023 · 1 comment
Open

Compiling flat vector doesn't terminate #7

eayus opened this issue Jan 4, 2023 · 1 comment

Comments

@eayus
Copy link

eayus commented Jan 4, 2023

Not sure whether this is known behaviour, but compileing the following example doesn't terminate (it checks fine)

data Nat where
  Zero : Nat
  Succ : Nat -> Nat

Pair : Type -> Type -> Type

data Pair a b where
  MkPair : a -> b -> Pair a b

data Unit where
  MkUnit : Unit

Vector : Nat -> Type -> Type
Vector Zero _ = Unit
Vector (Succ n) a = Pair a (Vector n a)
@ollef
Copy link
Owner

ollef commented Jan 4, 2023

Hey, and thanks for reaching out! The backend is quite unfinished, so I'm not too surprised at this stage. Most of my effort has gone into the type checker so far, but I'm hoping to do more work on the backend eventually. :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants