[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
14 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies,                      |
  PartialTypeSignatures              |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13877
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 (Originally spun off from #13877.)

 The following program gives a somewhat decent error message in GHC 8.0.1:

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

 import Data.Kind

 data family Sing (a :: k)

 data WeirdList :: Type -> Type where
   WeirdNil  :: WeirdList a
   WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a

 data instance Sing (z :: WeirdList a) where
   SWeirdNil  :: Sing WeirdNil
   SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)

 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
                         (p :: forall (x :: Type). x -> WeirdList x ->
 Type).
                  Sing wl
               -> (forall (y :: Type). p _ WeirdNil)
               -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList
 z)).
                     Sing x -> Sing xs -> p _ xs
                   -> p _ (WeirdCons x xs))
               -> p _ wl
 elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
 elimWeirdList (SWeirdCons (x :: Sing (x :: z))
                           (xs :: Sing (xs :: WeirdList (WeirdList z))))
               pWeirdNil pWeirdCons
   = pWeirdCons @z @x @xs x xs
       (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
 }}}

 {{{
 $ /opt/ghc/8.0.1/bin/ghci Foo.hs
 GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Foo.hs, interpreted )

 Foo.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
                                        -> (forall y. p x0 t3 'WeirdNil)
                                        -> (forall z (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                            Sing x
                                            -> Sing xs
                                            -> p (WeirdList z) t2 xs
                                            -> p z t1 ('WeirdCons x xs))
                                        -> p a t0 wl’
       to a visible type argument ‘WeirdList z’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
       In the expression:
         pWeirdCons
           @z
           @x
           @xs
           x
           xs
           (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
       In an equation for ‘elimWeirdList’:
           elimWeirdList
             (SWeirdCons (x :: Sing (x :: z))
                         (xs :: Sing (xs :: WeirdList (WeirdList z))))
             pWeirdNil
             pWeirdCons
             = pWeirdCons
                 @z
                 @x
                 @xs
                 x
                 xs
                 (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil
 pWeirdCons)
 }}}

 But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:

 {{{
 $ /opt/ghc/8.0.2/bin/ghci Foo.hs
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Foo.hs, interpreted )

 Foo.hs:24:41: error:
     • Found type wildcard ‘_’ standing for ‘t0’
       Where: ‘t0’ is an ambiguous type variable
              ‘x0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
     • Relevant bindings include
         elimWeirdList :: Sing wl
                          -> (forall y. p x0 t0 'WeirdNil)
                          -> (forall z (x :: z) (xs :: WeirdList (WeirdList
 z)).
                              Sing x
                              -> Sing xs -> p (WeirdList z) t1 xs -> p z t2
 ('WeirdCons x xs))
                          -> p a t3 wl
           (bound at Foo.hs:29:1)

 Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
   (GHC version 8.0.2 for x86_64-unknown-linux):
         No skolem info: z_a13X[sk]
 }}}

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Foo.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Foo.hs, interpreted )

 Foo.hs:21:18: error:
     • The kind of variable ‘wl1’, namely ‘WeirdList a1’,
       depends on variable ‘a1’ from an inner scope
       Perhaps bind ‘wl1’ sometime after binding ‘a1’
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 Foo.hs:24:41: error:
     • Found type wildcard ‘_’ standing for ‘w0’
       Where: ‘w0’ is an ambiguous type variable
              ‘x0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 24 |               -> (forall (y :: Type). p _ WeirdNil)
    |                                         ^

 Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
   (GHC version 8.2.1 for x86_64-unknown-linux):
         No skolem info:
   z_a1sY[sk:2]
   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/TcErrors.hs:2653:5 in
 ghc:TcErrors
 }}}

 (The error messages from HEAD, at commit
 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040>
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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 OK I understand the problem.  Consider the type signature (abbreviated
 from the one written)
 {{{
 -- Sing :: forall (a:*). WeirdList a -> *

 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
                         (p :: forall (x :: Type). x -> WeirdList x ->
 Type).
                  Sing wl
                  -> (forall (z :: Type) (x :: z) (xs :: WeirdList
 (WeirdList z)).
                        Sing x -> Sing xs -> p _ xs
                                             -- p @ (WeirdList z) (_ ::
 WeirdList z) xs
                      -> p _ (WeirdCons x xs))
                  -> p _ wl
 }}}
 I have written ou the explicitly kind application needed in the
 application `(p _ xs)`.

 Now remember that a signature with wildcards is like a template imposed on
 type inference.  The `_` wildcards are replaced with unification
 variables.  So it's like this
 {{{
 alpha1 :: kappa1
 alpha2 :: kappa2
 alpha3 :: kappa3

 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
                         (p :: forall (x :: Type). x -> WeirdList x ->
 Type).
                  Sing wl
                  -> (forall (z :: Type) (x :: z) (xs :: WeirdList
 (WeirdList z)).
                        Sing x -> Sing xs -> p alpha1 xs
                                             -- p @ (WeirdList z) (alpha1
 :: WeirdList z) xs
                      -> p alpha2 (WeirdCons x xs))
                  -> p alpah3 wl
 }}}
 These unification variables are at the "top" of the type.  Once you see
 this it is clear that simply kind-checking this type should fail, becuase
 `alpha` must have kind `WeirdList z`, and `z` is bound by that inner
 forall. Yikes!

 This is all happening because we aren't generating an implication
 constraint when we kind-check a forall.  In fact, there are other symptoms
 of the same problem: see #14066.  Let's cure that first, and then come
 back to this one (which might "just work").

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Another program with a similar structure and error message:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind

 data Proxy a = Proxy
 data family Sing (a :: k)

 data SomeSing k where
   SomeSing :: Sing (a :: k) -> SomeSing k

 class SingKind k where
   type Demote k :: Type
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k

 data instance Sing (x :: Proxy k) where
   SProxy :: forall (a :: k). Sing ('Proxy :: Proxy a)

 instance SingKind (Proxy k) where
   type Demote (Proxy k) = Proxy k
   fromSing SProxy = Proxy
   toSing Proxy = SomeSing SProxy

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

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

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }

 instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
   type Demote (k1 ~> k2) = Demote k1 -> Demote k2
   fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing
 sFun y)
   toSing = undefined

 dapp :: forall (a :: Type)
                (f :: forall (x :: a). Proxy x ~> Type)
                (x :: a).
         Sing f
      -> Sing x
      -> f @@ ('Proxy :: Proxy x)
 dapp f x = case f of
             SLambda (sF :: _) -> undefined
 }}}

 This time, all GHCs from 8.0.1 on give a similar panic:

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:56:28: error:
     • Found type wildcard ‘_’
         standing for ‘Singghc: panic! (the 'impossible' happened)
   (GHC version 8.2.1 for x86_64-unknown-linux):
         No skolem info:
   a1_a1tE[sk:1]
   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/TcErrors.hs:2653:5 in
 ghc:TcErrors
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Interestingly, the original program no longer panics on GHC HEAD, but the
 program in comment:2 still panics, this time with a slightly different
 panic:

 {{{
 GHCi, version 8.5.20171205: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

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

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

 Is it worth adding a regression test for the original program, or should I
 wait until the program in comment:2 has been fixed as well?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * owner:  (none) => goldfire


Comment:

 By all means add a regression test, thanks.  The more the better.

 Richard is actively working on a "solveEqualities" patch that will (I
 hope) fix this bug among many others (e.g. #14066)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies, PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Ryan Scott <ryan.gl.scott@…>):

 In [changeset:"be1ca0e439e9d26107c7d82fe6e78b64ee6320a9/ghc"
 be1ca0e4/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="be1ca0e439e9d26107c7d82fe6e78b64ee6320a9"
 Add regression test for #14040

 This adds a regression test for the original program in #14040.

 This does not fix #14040 entirely, though, as the program in
 https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2 still
 panics, so there is more work to be done there.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:  TypeInType, TypeFamilies, PartialTypeSignatures => TypeInType,
     TypeFamilies, PartialTypeSignatures, TypedHoles


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I regret to report that even after Richard's "solveEqualties" patch
 #14066, the example in comment:2 yields
 {{{
 T14040.hs:91:28: error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180402 for x86_64-unknown-linux):
         No skolem info:
   [a1_aWV[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
 }}}
 This arises during the error-report-generation stage.  The residual
 constraint is this
 {{{
 reportUnsolved (after zonking):
   Free tyvars: (t_a1e3[tau:2] :: Proxy x_a1dP[sk:2]) a_aWV[sk:1]
   Tidy env: ([ESf6y :-> 1, ESf7a :-> 1, ESfO0 :-> 2,
               ESgiS :-> 1],
              [aWV :-> a1_aWV[sk:1], a1dP :-> x_a1dP[sk:2],
               a1dQ :-> a_a1dQ[sk:2], a1e3 :-> t0_a1e3[tau:2]])
   Wanted: WC {wc_impl =
                 Implic {
                   TcLevel = 2
                   Skolems = (x_a1dP[sk:2] :: a_aWV[sk:1])
                             a_a1dQ[sk:2]
                             (f_a1dR[sk:2] :: forall (x :: a_a1dQ[sk:2]).
 Proxy x ~> *)
                             (x_a1dS[sk:2] :: a_a1dQ[sk:2])
                   No-eqs = True
                   Status = Unsolved
                   Given =
                   Wanted =
                     WC {wc_simple =
                           [D] _ {0}:: Sing t_a1e3[tau:2]
                                       -> Sing
                                            (Apply
                                               (f_a1dR[sk:2] x_a1dP[sk:2])
                                               t_a1e3[tau:2]) (CHoleCan:
 TypeHole(_))}
                   Binds = EvBindsVar<a2gv>
                   Needed inner = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
                                   a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
 :-> co_a2hR,
                                   a2hS :-> co_a2hS, a2i2 :-> $dIP_a2i2]
                   Needed outer = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
                                   a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
 :-> co_a2hR,
                                   a2hS :-> co_a2hS]
                   the type signature for:
                     dapp :: forall (x :: a_aWV[sk:1]) a (f :: forall (x ::
 a).
                                                               Proxy x ~>
 *) (x :: a).
                             Sing (f x) -> Sing x -> f x @@ 'Proxy }
 }}}
 And indeed you can see that the skolem `a1_aWV` is not bound by any
 implication.  This must be a bug.

 Richard?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Well I'll be danged—it looks like this no longer panics on GHC HEAD!

 {{{
 $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.5.20180413: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:21:18: error:
     • Couldn't match type ‘k0’ with ‘a’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
                                                                 x ->
 WeirdList x -> *).
                            Sing wl
                            -> (forall y. p k0 w0 'WeirdNil)
                            -> (forall z1 (x :: z1) (xs :: WeirdList
 (WeirdList z1)).
                                Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                            -> p k3 w3 wl
         at Bug.hs:(21,18)-(28,23)
       Expected type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
         Actual type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
     • In the ambiguity check for ‘elimWeirdList’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 Bug.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
                                        -> (forall y. p k0 w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs ::
 WeirdList (WeirdList z1)).
                                            Sing x
                                            -> Sing xs -> p k1 w1 xs -> p
 k2 w2 ('WeirdCons x xs))
                                        -> p k3 w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
       In the expression:
         pWeirdCons
           @z
           @x
           @xs
           x
           xs
           (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
       In an equation for ‘elimWeirdList’:
           elimWeirdList
             (SWeirdCons (x :: Sing (x :: z))
                         (xs :: Sing (xs :: WeirdList (WeirdList z))))
             pWeirdNil
             pWeirdCons
             = pWeirdCons
                 @z
                 @x
                 @xs
                 x
                 xs
                 (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil
 pWeirdCons)
    |
 34 |       (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 I'll confirm which commit caused this and add a regression test.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Never mind, I'm an idiot. I was looking at the original program, not the
 program in comment:2.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Here is a much simpler way to trigger the panic in comment:2:

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

 import Data.Kind
 import Data.Proxy

 newtype S (f :: k1 -> k2)
   = MkS (forall t. Proxy t -> Proxy (f t))

 foo :: forall (a :: Type)
               (f :: forall (x :: a). Proxy x -> Type).
        S f -> ()
 foo (MkS (sF :: _)) = ()
 }}}
 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
 GHCi, version 8.5.20180420: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:15:17: error:ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180420 for x86_64-unknown-linux):
         No skolem info:
   [a1_a1Cb[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
 }}}

 But it now appears that this bug is of a different nature than the
 original program. I'll close this ticket in favor of a new one.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:  fixed             |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:  partial-
  crash or panic                     |  sigs/should_fail/T14040a
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877, #15076    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * testcase:   => partial-sigs/should_fail/T14040a
 * status:  new => closed
 * resolution:   => fixed
 * related:  #13877 => #13877, #15076
 * milestone:   => 8.6.1


Comment:

 Closing in favor of #15076.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:  fixed             |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:  partial-
  crash or panic                     |  sigs/should_fail/T14040a
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877, #15076    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 There's still something wrong here, in the original program.  Even if we
 write
 {{{
 elimWeirdList x = error "urk"
 }}}
 GHC HEAD still complains mysteriously about the type signature
 {{{
 T14040a.hs:21:18: error:
     • Couldn't match type ‘k0’ with ‘a’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
                                                                 x ->
 WeirdList x -> *).
                            Sing wl
                            -> (forall y. p k0 w0 'WeirdNil)
                            -> (forall z1 (x :: z1) (xs :: WeirdList
 (WeirdList z1)).
                                Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                            -> p k3 w3 wl
         at T14040a.hs:(21,18)-(28,23)
       Expected type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
         Actual type: Sing wl
                      -> (forall y. p k1 w0 'WeirdNil)
                      -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList
 z1)).
                          Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2
 ('WeirdCons x xs))
                      -> p k3 w3 wl
     • In the ambiguity check for ‘elimWeirdList’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

 T14040a.hs:29:1: error:
     Can't quantify over ‘a’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 T14040a.hs:29:1: error:
     Can't quantify over ‘wl’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 T14040a.hs:29:1: error:
     Can't quantify over ‘p’
       bound by the partial type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
                                 (p :: forall (x :: Type). x -> WeirdList x
 -> Type).
                          Sing wl
                          -> (forall (y :: Type). p _ WeirdNil)
                             -> (forall (z :: Type) (x :: z) (xs ::
 WeirdList (WeirdList z)).
                                 Sing x -> Sing xs -> p _ xs -> p _
 (WeirdCons x xs))
                                -> p _ wl
    |
 29 | elimWeirdList x = error "urk"
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies,
                                     |  PartialTypeSignatures, TypedHoles
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:  partial-
  crash or panic                     |  sigs/should_fail/T14040a
      Blocked By:                    |             Blocking:
 Related Tickets:  #13877, #15076    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  closed => new
 * owner:  goldfire => (none)
 * resolution:  fixed =>


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#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