#1965: Allow unconstrained existential contexts in newtypes -------------------------------------+------------------------------------- Reporter: guest | Owner: Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 6.8.1 Component: Compiler | Keywords: Resolution: | Operating System: Unknown/Multiple Differential Revisions: | Type of failure: None/Unknown Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Comment (by pumpkin): Dan Doel pointed out that as useful as this could be, it would allow this fairly odd use case: {{{ #!haskell data Nat = Z | S Nat data Fin n where Zero :: Fin (S n) Suc :: Fin n -> Fin (S n) newtype SomeFin where SomeFin :: Fin n -> SomeFin suc :: SomeFin -> SomeFin suc (SomeFin n) = SomeFin (Suc n) inf :: SomeFin inf = suc inf }}} Which leads to `inf` containing a `Fin` whose existential index can't actually be any valid (finite) type. `Fin` thus becomes a bit of a misnomer in this context, since it's not finite. Making `SomeFin` into data rather than newtype fixes the problem by making `inf` into a bottom. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/1965#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler