[GHC] #14880: GHC panic: updateRole

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
155 messages Options
1234 ... 8
Reply | Threaded
Open this post in threaded view
|

[GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:  Roles          |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality ((:~:)(..))

 type SameKind (a :: k) (b :: k) = (() :: Constraint)

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type f @@ x = f `Apply` x
 infixl 9 @@

 type family WhyCong (x :: Type) (y :: Type) (f :: x ~> y)
                     (a :: x) (z :: x) (e :: a :~: z) :: Type where
   WhyCong _ _ f a z _ = f @@ a :~: f @@ z

 data WhyCongSym1 (x :: Type) :: forall (a :: x)
                                        (y :: Type)
                                        (z :: x).
                                 Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~>
 Type

 data WhyCongSym0 :: forall (x :: Type)
                            (a :: x)
                            (y :: Type)
                            (z :: x).
                     Type ~> Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~> Type
   where
     WhyCongSym0KindInference :: forall x arg.
                                 SameKind (Apply WhyCongSym0 arg)
 (WhyCongSym1 arg) =>
                                 WhyCongSym0 x
 }}}

 {{{
 $ /opt/ghc/8.2.2/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.2 for x86_64-unknown-linux):
         updateRole
   WhyCongSym0
   arg_aYV[sk:1]
   [aYU :-> 4, a22o :-> 0, a22p :-> 1, a22q :-> 2, a22r :-> 3]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in
 ghc:TcTyDecls
 }}}

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  Roles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

Old description:

> The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
>
> {{{#!hs
> {-# LANGUAGE ConstraintKinds #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE TypeInType #-}
> {-# LANGUAGE TypeOperators #-}
> module Bug where
>
> import Data.Kind
> import Data.Type.Equality ((:~:)(..))
>
> type SameKind (a :: k) (b :: k) = (() :: Constraint)
>
> data TyFun :: Type -> Type -> Type
> type a ~> b = TyFun a b -> Type
> infixr 0 ~>
>
> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
> type f @@ x = f `Apply` x
> infixl 9 @@
>
> type family WhyCong (x :: Type) (y :: Type) (f :: x ~> y)
>                     (a :: x) (z :: x) (e :: a :~: z) :: Type where
>   WhyCong _ _ f a z _ = f @@ a :~: f @@ z
>
> data WhyCongSym1 (x :: Type) :: forall (a :: x)
>                                        (y :: Type)
>                                        (z :: x).
>                                 Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~>
> Type
>
> data WhyCongSym0 :: forall (x :: Type)
>                            (a :: x)
>                            (y :: Type)
>                            (z :: x).
>                     Type ~> Type ~> (x ~> y) ~> x ~> x ~> a :~: z ~> Type
>   where
>     WhyCongSym0KindInference :: forall x arg.
>                                 SameKind (Apply WhyCongSym0 arg)
> (WhyCongSym1 arg) =>
>                                 WhyCongSym0 x
> }}}
>
> {{{
> $ /opt/ghc/8.2.2/bin/ghc Bug.hs
> [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
> ghc: panic! (the 'impossible' happened)
>   (GHC version 8.2.2 for x86_64-unknown-linux):
>         updateRole
>   WhyCongSym0
>   arg_aYV[sk:1]
>   [aYU :-> 4, a22o :-> 0, a22p :-> 1, a22q :-> 2, a22r :-> 3]
>   Call stack:
>       CallStack (from HasCallStack):
>         prettyCurrentCallStack, called at
> compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
>         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
> ghc:Outputable
>         pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in
> ghc:TcTyDecls
> }}}
New description:

 The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality ((:~:))

 type SameKind (a :: k) (b :: k) = (() :: Constraint)

 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

 data WhyCongSym1 (x :: Type) :: forall (a :: x)
                                        (y :: Type)
                                        (z :: x).
                                 Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~>
 Type

 data WhyCongSym0 :: forall (x :: Type)
                            (a :: x)
                            (y :: Type)
                            (z :: x).
                     Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~>
 Type
   where
     WhyCongSym0KindInference :: forall x arg.
                                 SameKind (Apply WhyCongSym0 arg)
 (WhyCongSym1 arg) =>
                                 WhyCongSym0 x
 }}}

 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.2 for x86_64-unknown-linux):
         updateRole
   WhyCongSym0
   arg_a1A6[sk:1]
   [a1A5 :-> 4, a2Cy :-> 0, a2Cz :-> 1, a2CA :-> 2, a2CB :-> 3]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in
 ghc:TcTyDecls
 }}}

--

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  Roles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Here's as minimal of an example as I can conjure up:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

 data Bar :: Type -> Type where
     MkBar :: forall x arg.
              -- Commenting out the line below makes the issue go away
              Foo arg ~ Foo arg =>
              Bar x
 }}}
 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.2 for x86_64-unknown-linux):
         updateRole
   Bar
   arg_a1vT[sk:1]
   [a1vS :-> 0]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in
 ghc:TcTyDecls
 }}}

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  Roles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Even simpler
 {{{
  data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

  data Bar :: Type -> Type where
      MkBar :: forall x arg.
               -- Commenting out the line below makes the issue go away
               Proxy (Foo arg) ->
               Bar x
 }}}
 The panic is caused because the existentials for `MkBar` are messed up;
 {{{
 {-  MkBar
     univ_tvs:   (x :: *)
     ex_tvs:     (a :: arg_aZv)
                 (arg_XZx :: *)
     arg ty:     Proxy @arg_XZx a
     result ty:  Foo @arg_XZx a
 }}}
 Note the confusion of two `arg` variables.  Ran out of time at that point.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * keywords:  Roles => TypeInType
 * owner:  (none) => goldfire


Comment:

 The trouble is that the type of `MkBar` should really be
 {{{
 MkBar :: forall (x:Type) (arg:Type) {a:arg}.
          Proxy @(Proxy @arg a -> Type)
                (Foo arg @a)
       -> Bar x
 }}}
 where I have put in all the kind applications.  The trouble is that
 `MkBar` has an ''implicit'' forall's variable `a`, whose kind mentions
 an ''explicit'' type variable `arg`.
 So the implicit argument must appear later in the telescope.
 But `tcConDecl` (the `ConDeclGADT` case) doesn't allow that:
 {{{
              tkv_bndrs      = mkTyVarBinders Inferred  tkvs'
              user_tv_bndrs  = mkTyVarBinders Specified user_tvs'
              all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
 }}}
 Notice that the inferred ones always come first.  But here they can't!

 Solution: do a topo-sort of the tyvars that is allowed to interleave
 the `Inferred` and `Specified` ones.

 But is that the only place?
 If we try something like this with a function type signature thus
 {{{
 f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a
 f = f
 }}}
 we get the error message
 {{{
 T14880.hs:24:6: error:
     * The kind of variable `k', namely `v',
       depends on variable `v' from an inner scope
       Perhaps bind `k' sometime after binding `v'
       NB: Implicitly-bound variables always come before other ones.
     * In the type signature:
         f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a
 }}}
 But is there anything really wrong with this signature? It we topo-sorted
 the type variables we'd be fine.

 There are other places (exp in `TcTyClsDecls`) where we seem to put all
 the
 inferred variables around the outside.  I don't know how to be sure in
 which, if
 any, of these case we have a bug.  Maybe we need more topo-sorts?

 Amnother oddd thing about this ticket is the data decl for `Foo`:
 {{{
 data Foo (v :: Type) :: forall (a :: v). Proxy a -> Type
 }}}
 That is a strange kind signature. I don't expect to see foralls to the
 right of the `::` in such a decl.  So, more questions

 * Is it valuable to permit TyCons whose kinds are not in prenex form (i.e.
 all foralls at the front)?

 If so, we should document it.

 Meanwhile I'm not going to fix this because it may all come out in the
 wash
 of Richards's upcoming kind-inference patch.


 It's nothing to do with roles!

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 The `updateRole` panic triggers on various invalid-tycon problems. I'm not
 surprised that roles aren't involved.

 Yes, a `forall` to the right of the `::` in a data declaration makes fine
 sense. For example, here is one way to define heterogeneous equality:

 {{{#!hs
 data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
   HRefl :: a :~~: a
 }}}

 This definition is actually a touch more general than one where `k1` and
 `k2` are quantified prenex, as the "Practical Type Inference" paper
 explains.

 I don't see a need to document this specially.

 As for the toposorting suggestions: I've considered it a design principle
 that implicit quantification comes before all explicit quantification. Of
 course, we can't panic when something goes wrong here, but I think this
 design is a good one, just to have some rules that users can rely on.

 My existing patch still panics on this case, but I agree that no one
 should spend time on this until that patch lands.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 With the `Foo` in comment:3, this also panics:

 {{{#!hs
 quux :: forall x arg. Proxy (Foo arg) -> Maybe x
 quux = undefined
 }}}

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:6 goldfire]:
 > With the `Foo` in comment:3, this also panics:

 It does? I must be doing something wrong, since this appears to compile
 for me:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

 quux :: forall x arg. Proxy (Foo arg) -> Maybe x
 quux = undefined
 }}}

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 >  My existing patch still panics on this case, but I agree that no one
 should spend time on this until that patch lands.

 Richard, now that the patch has landed, and this stuff is in your head,
 might you look at this?  I doubt it's hard.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * related:   => #15076


Comment:

 I think that this ticket and #15076 share a symptom in common. This claim
 is based on the fact that slightly tweaking the program in comment:6 /
 comment:7 :

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

 quux :: forall arg. Proxy (Foo arg) -> ()
 quux (_ :: _) = ()
 }}}

 Yields:

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:12:12: error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180420 for x86_64-unknown-linux):
         No skolem info:
   [arg_aZr[sk:1]]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in
 ghc:Outputable
         pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in
 ghc:TcErrors
 }}}

 Which is the same panic as in #15076. Plus, if you run this program with
 `-ddump-tc-trace`, you see:

 {{{
 reportUnsolved (after zonking):
   Free tyvars: arg_aZr[sk:1]
   Tidy env: ([ESf71 :-> 1], [aZr :-> arg_aZr[sk:1]])
   Wanted: WC {wc_impl =
                 Implic {
                   TcLevel = 2
                   Skolems = (a_a1p8[sk:2] :: arg_aZr[sk:1]) arg_a1p9[sk:2]
                   No-eqs = True
                   Status = Unsolved
                   Given =
                   Wanted =
                     WC {wc_simple =
                           [D] _ {0}:: Proxy
                                         (Foo arg_a1p9[sk:2] a_a1p8[sk:2])
 (CHoleCan: TypeHole(_))}
                   Binds = EvBindsVar<a1pg>
                   Needed inner = []
                   Needed outer = []
                   the type signature for:
                     quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo
 arg a) -> () }}
 }}}

 Just like in #15076, `arg_aZr` is not bound in any implication. On the
 other hand, there is another type variable, `arg_a1p9`, that is
 suspiciously similar. Moreover, the type signature it gives for `quux`:

 {{{
 quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo arg a) -> ()
 }}}

 Seems to have //two// different copies of `arg`! This is especially
 interesting in light of comment:3, where simonpj discovered that the
 existentially quantified tyvars in `MkBar` were screwed up, leading to two
 copies of `arg`.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 >  The trouble is that MkBar has an implicit forall's variable a, whose
 kind mentions an explicit type variable arg.

 Richard and I discussed this on Monday.  Our conclusions

 * `Inferred` variables should always precede `Specified` ones.  That is,
 do not top-sort

 * Idea: simply refrain from quantifying any inferred variables that
 mention specified ones.  They'll get defaulted to `Any` which is probably
 fine.  This refraining can readily be done in `candidatesQTyVarsOfType`.

 * Also came up: close over kinds once in `tyCoVarsOfType` instead of at
 every leaf. This is not just an efficiency issue: consider
 {{{
 tyCoVarsOfType (forall a. b::a)
 }}}
 Richard is on the job

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Trac #15076 is another example of the same phenomenon.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 And probably #14040 too.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Yes, I have a fix
 [https://github.com/goldfirere/ghc/commit/7386ea571cdd50d45432e20a5318e7e870f0176b
 here], but it causes a failure in, e.g., indexed-
 types/should_compile/T12369. Haven't had time to investigate.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Maybe #14887 too!

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * blocking:  15170 =>


Comment:

 I believe that #15170 is also blocked on this.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 In a call today Richard and Simon decided:

 * Kill 1decideKindGeneralisationPlan`; instead always generalise. (Explain
 why we don't need to worry about local generalisation as we do with
 terms.)

 * And hence kill `tc_hs_sig_type`, leaving `tc_hs_sig_type_and_gen`

 * `tc_hs_sig_type_and_gen` should not call `solveEqualities` (which fails
 if there are unsolved equalities)

 * Instead call `solveLocalEqualities`, gather unsolved equalities, and do
 not quantify over their free vars.   NB: `tcImplicitTKBndrs` already calls
 `solveLocalEqualities`, and must do so.  Needs a Note to explain why: it's
 so that we can top-sort the bound variables

 * Promote all the free vars of the unsolved constraints. '''Principle''':
 all free vars should either be generalised or promoted.

 * Get rid of `zonkPromote` and friends altogether

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 While I agree with comment:17, that doesn't have anything to do with this
 ticket...

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):  Phab:D4769
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * differential:   => Phab:D4769


Comment:

 Since my last update, the patch in Phab:D4769 works but has performance
 trouble. I've asked Ben & friends for help.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14880: GHC panic: updateRole

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14880: GHC panic: updateRole
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15076            |  Differential Rev(s):  Phab:D4769
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by tdammers):

 Could you maybe provide a quick summary of the exact performance trouble?
 I'm running some tests as we speak, but it would be easier for me if you
 could hint at some tests that produce particularly bad behavior, or maybe
 an example program on which GHC peforms badly after this patch.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
1234 ... 8