#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