Opened 2 years ago

Last modified 7 months ago

#14040 new bug

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.0.2
Keywords: TypeInType, TypeFamilies, PartialTypeSignatures, TypedHoles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: partial-sigs/should_fail/T14040a
Blocked By: Blocking:
Related Tickets: #13877, #15076 Differential Rev(s):
Wiki Page:

Description

(Originally spun off from #13877.)

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

{-# 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.)

Change History (19)

comment:1 Changed 2 years ago 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").

comment:2 Changed 2 years ago by RyanGlScott

Another program with a similar structure and error message:

{-# 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

comment:3 Changed 21 months ago 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?

comment:4 Changed 21 months ago by simonpj

Owner: set to goldfire

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)

comment:5 Changed 21 months ago by Ryan Scott <ryan.gl.scott@…>

In be1ca0e4/ghc:

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.

comment:6 Changed 18 months ago by RyanGlScott

Keywords: TypedHoles added

comment:7 Changed 18 months ago 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?

comment:8 Changed 17 months ago 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.

comment:9 Changed 17 months ago by RyanGlScott

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

Last edited 17 months ago by RyanGlScott (previous) (diff)

comment:10 Changed 17 months ago by RyanGlScott

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

{-# 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.

comment:11 in reply to:  7 Changed 17 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: partial-sigs/should_fail/T14040a

Closing in favor of #15076.

comment:12 Changed 16 months ago 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"
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

comment:13 Changed 16 months ago by simonpj

Owner: goldfire deleted
Resolution: fixed
Status: closednew

comment:14 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed by GHC 8.6.

comment:15 Changed 11 months ago by RyanGlScott

simonpj, isn't it expected that GHC would complain if you implemented elimWeirdList as elimWeirdList x = error "urk"? After all, elimWeirdList contains higher-rank arguments, and trying to instantiate them with error "urk" :: forall a. a would require instantiating a with a polytype, which is impredicative.

Also, it's worth noting that on GHC HEAD, you get one fewer error than you do in comment:12:

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

Bug.hs:37: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
   |
37 | elimWeirdList x = error "urk"
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:37: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
   |
37 | elimWeirdList x = error "urk"
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:37: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
   |
37 | elimWeirdList x = error "urk"
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

comment:16 Changed 10 months ago by RyanGlScott

The error message has changed once again in GHC HEAD (as of commit 2257a86daa72db382eb927df12a718669d5491f8):

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

../Bug.hs:34:8: error:
    • Cannot apply expression of type ‘Sing wl0
                                       -> (forall y. p0 w0 'WeirdNil)
                                       -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
                                           Sing x -> Sing xs -> p0 w1 xs -> p0 w2 ('WeirdCons x xs))
                                       -> p0 w3 wl0’
      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)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

comment:17 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:18 Changed 7 months ago by RyanGlScott

The error message for the error "urk" version has changed once again in GHC HEAD. Simon, can you spot-check this to see if this looks correct? (Modulo wildcard pretty-printing, of course.)

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

Bug.hs:24:41: error:
    • Found type wildcard ‘_’ standing for ‘_1 :: x0’
      Where: ‘x0’ is an ambiguous type variable
             ‘_1’ is an ambiguous type variable
      To use the inferred type, enable PartialTypeSignatures
    • In the first argument of ‘p’, namely ‘_’
      In the 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’
      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)
   |                                         ^

Bug.hs:26:44: error:
    • Found type wildcard ‘_’
        standing for ‘GHC.Types.Any :: WeirdList z’
      Where: ‘z’ is a rigid type variable bound by
               ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
                Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
               at Bug.hs:25:27
      To use the inferred type, enable PartialTypeSignatures
    • In the first argument of ‘p’, namely ‘_’
      In the 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’
      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
   |
26 |                     Sing x -> Sing xs -> p _ xs
   |                                            ^

Bug.hs:27:24: error:
    • Found type wildcard ‘_’ standing for ‘GHC.Types.Any :: z’
      Where: ‘z’ is a rigid type variable bound by
               ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
                Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
               at Bug.hs:25:27
      To use the inferred type, enable PartialTypeSignatures
    • In the first argument of ‘p’, namely ‘_’
      In the 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’
      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
   |
27 |                   -> p _ (WeirdCons x xs))
   |                        ^

Bug.hs:28:20: error:
    • Found type wildcard ‘_’ standing for ‘_0 :: a’
      Where: ‘a’ is an ambiguous type variable
             ‘_0’ is an ambiguous type variable
      To use the inferred type, enable PartialTypeSignatures
    • In the first argument of ‘p’, namely ‘_’
      In the 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’
      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
   |
28 |               -> p _ wl
   |                    ^

Bug.hs:37:19: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls:
        (forall y. p _1 'WeirdNil)
        -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
            Sing x
            -> Sing xs
            -> p GHC.Types.Any xs
            -> p GHC.Types.Any ('WeirdCons x xs))
        -> p _0 wl
        GHC doesn't yet support impredicative polymorphism
    • In the expression: error "urk"
      In an equation for ‘elimWeirdList’: elimWeirdList x = error "urk"
    • Relevant bindings include
        x :: Sing wl (bound at Bug.hs:37:15)
        elimWeirdList :: Sing wl
                         -> (forall y. p _1 'WeirdNil)
                         -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
                             Sing x
                             -> Sing xs
                             -> p GHC.Types.Any xs
                             -> p GHC.Types.Any ('WeirdCons x xs))
                         -> p _0 wl
          (bound at Bug.hs:37:1)
   |
37 | elimWeirdList x = error "urk"
   |                   ^^^^^^^^^^^

comment:19 Changed 7 months ago by simonpj

The original program now reports just one error

T14040.hs:41:8: error:
    • Cannot apply expression of type ‘Sing wl0
                                       -> (forall y. p0 _0 'WeirdNil)
                                       -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
                                           Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs))
                                       -> p0 _3 wl0’
      to a visible type argument ‘(WeirdList z)’

And that's right: the signature for elimWierdList is a partial signature, so we do inference on the definition. So at the recursive call to elimWierdList, the function is a monotype, and can't be applied to type arguments.

However, for the elimWierdList x = error "urk" version I get

WARNING: file compiler/types/TyCoRep.hs, line 3033
  in_scope InScope {a_a10j wl_a10k p_a10l}
  tenv [aX1 :-> a_a10j[tyv:1], aX2 :-> wl_a10k[tyv:1],
        aX4 :-> p_a10l[tyv:1]]
  cenv []
  tys [Sing wl_aX2[tyv:1]
       -> (forall y. p_aX4[tyv:1] __aZo[tau:2] 'WeirdNil)
       -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
           Sing x
           -> Sing xs
           -> p_aX4[tyv:1] __aZL[tau:2] xs
           -> p_aX4[tyv:1] __aZP[tau:2] ('WeirdCons x xs))
       -> p_aX4[tyv:1] __aZW[tau:1] wl_aX2[tyv:1]]
  cos []
  needInScope {z_aX6[sk:2], x_aZm[tau:2], __aZo[tau:2], __aZL[tau:2],
               __aZP[tau:2], __aZW[tau:1]}
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1211:29 in ghc:Outputable
        warnPprTrace, called at compiler/types/TyCoRep.hs:3027:6 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:3050:29 in ghc:TyCoRep
        substTy, called at compiler/typecheck/TcSigs.hs:507:49 in ghc:TcSigs
ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 8.7.20190215 for x86_64-unknown-linux):
	ASSERT failed!
  2
  0
  __a23h[tau:0]
  Any
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1220:5 in ghc:Outputable
        assertPprPanic, called at compiler/typecheck/TcMType.hs:805:54 in ghc:TcMType

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

So there is still stuff wrong here.

Note: See TracTickets for help on using tickets.