Hi Haskell Cafe! To develop Haskell-Type-Exts (HTE) [1,2], I need to have typing judgments for each language construct in Haskell 2010 with two extensions: RankNTypes and local assumptions (GADTs, Type Functions and etc). Since I could not find any academic paper describing a type system supporting both local assumptions [3] and RankNTypes [4], we tried to combine the two systems. We also tried to extend the type system to support Patterns and some other constructs. The result (in a very sketchy state) is posted at: http://cleantypecheck.wordpress.com/2012/06/06/typing-judgment-rules-14/ Now before I start to implement these rules in HTE, I need to make sure of their validity. Therefore, I'd highly appreciate if experts would take a closer look at these judgement rules and comment. Considering the fact that HTE is a Google SoC project and me being just a motivated student (limited knowledge/experience), the success of this project strongly relies on Haskell community's support. Thanks! /Shayan [1] http://www.google-melange.com/gsoc/project/google/gsoc2012/shayannajd/18001 [2] http://cleantypecheck.wordpress.com/2012/05/03/kickoff/ [3] D. Vytiniotis, S. Peyton Jones, T. Schrijvers, M. Sulzmann. OutsideIn(X) – Modular type inference with local assumptions [4] S. Peyton Jones, D. Vytiniotis, S. Weirich, and M. Shields. Practical type inference for arbitrary-rank types.