search

goldfirere / ghc

Mirror of ghc repository. DO NOT SUBMIT PULL REQUESTS HERE
http://www.haskell.org/ghc/
Other
25 stars 1 forks source link

Errors when defining Sigma #32

Closed RafaelBocquet closed 9 years ago

RafaelBocquet commented 9 years ago

I got these two bugs while trying to define de dependent sigma type :

module A where

data family Sing (k :: *) :: k -> *

data TyArr' (a :: *) (b :: *) :: *
type TyArr (a :: *) (b :: *) = TyArr' a b -> *
type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyArr a *) :: *
type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
$(return [])

data MkStar (p :: *) (x :: TyArr' p *)
type instance MkStar p @@ x = *
$(return [])

data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
  Sigma ::
    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
    Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r
$(return [])

data instance Sing Sigma (Sigma p r) x where
  SSigma ::
    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
    (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b).
    Sing (Sing (r @@@ a) b) sb ->
    Sing (Sigma p r) ('Sigma sp sr sa sb)
ghc: panic! (the 'impossible' happened)
  (GHC version 7.11.20150527 for x86_64-unknown-linux):
    ASSERT failed!
  file compiler/types/Coercion.hs line 1024
  Sym cobox_a3RY representational
module A where

data family Sing (k :: *) :: k -> *

data TyArr (a :: *) (b :: *) :: *
type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
$(return [])

data Sigma (p :: *) (r :: TyArr p * -> *) :: * where
  Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a).
           Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r
$(return [])

data instance Sing (Sigma p r) (x :: Sigma p r) :: * where
  SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a)
            (sp :: Sing * p) (sr :: Sing (TyArr p * -> *) r) (sa :: Sing p a) (sb :: Sing (r @@ a) b).
            Sing (Sing (r @@ a) b) sb ->
            Sing (Sigma p r) ('Sigma sp sr sa sb)
ghc: panic! (the 'impossible' happened)
  (GHC version 7.11.20150527 for x86_64-unknown-linux):
    ASSERT failed! file compiler/typecheck/TcCanonical.hs, line 1093
goldfirere commented 9 years ago

The first program above still panics, but it's a panic from the inability to create a proper error when there's an illegal GADT. The second program compiles. I'm closing.