[GHC] #1965: Allow unconstrained existential contexts in newtypes

[GHC]

#1965: Allow unconstrained existential contexts in newtypes
-------------------------------------+-------------------------------------
        Reporter:  guest             |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  6.8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Possible example from
 [http://www.cl.cam.ac.uk/~mpf23/papers/Types/gadtif.pdf A Foundation for
 GADTs and Inductive Families], encoding GADTs as left Kan extensions can
 be reworked to:

 {{{#!hs
 data N = O | S N

 data LanO j where
   LanO :: LanO (S i)

 data LanS j where
   LanS :: Fin i -> LanS (S i)
 }}}

 `Fin` defined as

 {{{#!hs
 data Fin a where
   FinO :: LanO i -> Fin i
   FinS :: LanS i -> Fin i

 pattern FinO'   = FinO LanO
 pattern FinS' n = FinS (LanS n)
 }}}

 Do `LanO`, `LanS` satisfy the conditions to be newtypes?

 === Original code===
 {{{#!hs
 data Fin :: * -> * where
   NZero :: Lan S One j -> Fin j
   NSucc :: Lan S Fin j -> Fin j

 data One j      = One
 data Lan h _X j = forall i. Lan (Eql j (h i), _X i)
 data Eql i j    where Refl :: Eql i i
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/1965#comment:31>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler