au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Non-exhaustive patterns in dargent implementation. #310

Open gteege opened 4 years ago

gteege commented 4 years ago

(I know that it's alpha and the example makes no sense, but when I hit it I can tell you anyways.)

type A
type BA = A layout 4B

causes the error message (when processed in dargent branch):

Parsing...
Resolving dependencies...
Typechecking...
cogent: src/Cogent/TypeCheck/Base.hs:(611,13)-(616,23): Non-exhaustive patterns in case

The same happens for

type R = { x: String } layout record { x: 4B }

although

type BA = String layout 4B

and

type A
type R = { x: A } layout record { x: 4B }

give useful error messages ("Layout does not match type").