google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

parsing of levelled forall types sometimes fails #38

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
What steps will reproduce the problem?
1. uncomment and try compiling these datatype definitions:
{-
-- unexpected "*" at: "(1+s)) . k..."
data Test :: level s . forall (k::*(1+s)) . k ~> * where
  T :: Test a
-}

looks like there must be a space between :: and *

{-
-- unexpected " +s)) . k ~> * where...
data Test :: level s . forall (k:: *(1 +s)) . k ~> * where
  T :: Test a
-}

looks like there must be *no* space between 1 and +

These problems seem to come from the parser.

I was using the Nov 8 snapshot.

Original issue reported on code.google.com by ggr...@gmail.com on 15 Nov 2007 at 10:50