[project @ 2005-10-14 11:22:41 by simonpj]
authorsimonpj <unknown>
Fri, 14 Oct 2005 11:22:42 +0000 (11:22 +0000)
committersimonpj <unknown>
Fri, 14 Oct 2005 11:22:42 +0000 (11:22 +0000)
commit36436bc62a98f53e126ec02fe946337c4c766c3f
tree575be956f1cc8ec8677c55b7a9ba37aceff494c3
parent8761b73561019d5514194fc8b0eee2b13f0e0ec9
[project @ 2005-10-14 11:22:41 by simonpj]
Add record syntax for GADTs
~~~~~~~~~~~~~~~~~~~~~~~~~~~

Atrijus Tang wanted to add record syntax for GADTs and existential
types, so he and I worked on it a bit at ICFP.  This commit is the
result.  Now you can say

 data T a where
  T1 { x :: a }             :: T [a]
  T2 { x :: a, y :: Int }   :: T [a]
  forall b. Show b =>
  T3 { naughty :: b, ok :: Int } :: T Int
  T4 :: Eq a => a -> b -> T (a,b)

Here the constructors are declared using record syntax.

Still to come after this commit:
  - User manual documentation
  - More regression tests
  - Some missing cases in the parser (e.g. T3 won't parse)
Autrijus is going to do these.

Here's a quick summary of the rules.  (Atrijus is going to write
proper documentation shortly.)

Defnition: a 'vanilla' constructor has a type of the form
forall a1..an. t1 -> ... -> tm -> T a1 ... an
No existentials, no context, nothing.  A constructor declared with
Haskell-98 syntax is vanilla by construction.  A constructor declared
with GADT-style syntax is vanilla iff its type looks like the above.
(In the latter case, the order of the type variables does not matter.)

* You can mix record syntax and non-record syntax in a single decl

* All constructors that share a common field 'x' must have the
  same result type (T [a] in the example).

* You can use field names without restriction in record construction
  and record pattern matching.

* Record *update* only works for data types that only have 'vanilla'
  constructors.

* Consider the field 'naughty', which uses a type variable that does
  not appear in the result type ('b' in the example).  You can use the
  field 'naughty' in pattern matching and construction, but NO
  SELECTOR function is generated for 'naughty'.  [An attempt to use
  'naughty' as a selector function will elicit a helpful error
  message.]

* Data types declared in GADT syntax cannot have a context. So this
is illegal:
data (Monad m) => T a where
  ....

* Constructors in GADT syntax can have a context (t.g. T3, T4 above)
  and that context is stored in the constructor and made available
  when the constructor is pattern-matched on.  WARNING: not competely
  implemented yet, but that's the plan.

Implementation notes
~~~~~~~~~~~~~~~~~~~~
- Data constructors (even vanilla ones) no longer share the type
  variables of their parent type constructor.

- HsDecls.ConDecl has changed quite a bit

- TyCons don't record the field labels and type any more (doesn't
  make sense for existential fields)

- GlobalIdDetails records which selectors are 'naughty', and hence
  don't have real code.
30 files changed:
ghc/compiler/basicTypes/DataCon.lhs
ghc/compiler/basicTypes/Id.lhs
ghc/compiler/basicTypes/IdInfo.lhs
ghc/compiler/basicTypes/MkId.lhs
ghc/compiler/coreSyn/CoreUnfold.lhs
ghc/compiler/coreSyn/CoreUtils.lhs
ghc/compiler/deSugar/DsArrows.lhs
ghc/compiler/deSugar/DsExpr.lhs
ghc/compiler/deSugar/Match.lhs
ghc/compiler/deSugar/MatchCon.lhs
ghc/compiler/hsSyn/HsDecls.lhs
ghc/compiler/hsSyn/HsUtils.lhs
ghc/compiler/iface/BuildTyCl.lhs
ghc/compiler/iface/TcIface.lhs
ghc/compiler/parser/Parser.y.pp
ghc/compiler/parser/ParserCore.y
ghc/compiler/parser/RdrHsSyn.lhs
ghc/compiler/rename/RnHsSyn.lhs
ghc/compiler/rename/RnSource.lhs
ghc/compiler/rename/RnTypes.lhs
ghc/compiler/simplCore/SimplUtils.lhs
ghc/compiler/specialise/Rules.lhs
ghc/compiler/stgSyn/StgLint.lhs
ghc/compiler/typecheck/TcExpr.lhs
ghc/compiler/typecheck/TcHsType.lhs
ghc/compiler/typecheck/TcTyClsDecls.lhs
ghc/compiler/typecheck/TcType.lhs
ghc/compiler/types/TyCon.lhs
ghc/compiler/types/Type.lhs
ghc/compiler/types/Unify.lhs