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

GHC ghc-devs at haskell.org
Sat Jul 19 05:15:03 UTC 2014


#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


More information about the ghc-tickets mailing list