Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#10432 closed bug (fixed)

panic with kind polymorphism

Reported by: Ashley Yakeley Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T10432
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1691
Wiki Page:

Description

{-# LANGUAGE ExistentialQuantification, PolyKinds,
DataKinds, RankNTypes, GADTs, TypeOperators #-}
module Bug where
import Data.Type.Equality

data WrappedType = forall a. WrapType a;

matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
  ('WrapType a :~: 'WrapType b) -> (('WrapType a ~ 'WrapType b) => r) -> r;
matchReflK Refl r = r;

give this:

Bug.hs:8:15:
    Couldn't match kind ‘ka’ with ‘kb’
      ‘ka’ is untouchable
        inside the constraints ('WrapType a ~ 'WrapType b)
        bound by the type signature for
                   matchReflK :: ('WrapType a ~ 'WrapType b) => r
        at Bug.hs:(8,15)-(9,74)ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.1 for x86_64-unknown-linux):
	No skolem info: ka_aqv[sk]

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

I actually think GHC should accept this (and furthermore infer ka ~ kb).

Change History (10)

comment:1 Changed 4 years ago by simonpj

This works in HEAD, but another variant makes HEAD, too, fail in the same way No skolem info:

matchReflK2 :: forall (a :: ka) (b :: kb) (r :: *).
              ('WrapType a :~: 'WrapType b) ->  r
matchReflK2 x
 = let foo :: ('WrapType a ~ 'WrapType b) => r
       foo = undefined
   in undefined

Reason: the type of foo mentions a, b, r as free variables; the ambiguity check doesn't bind them; the error message generator falls over.

Need to look into this.

comment:2 Changed 4 years ago by jstolarek

I just tested Simon's code and it works in HEAD. Originally reported code results in type ambiguity error (well, kind ambiguity in fact). 403cfc9187b9df560768bb809f4d280fb999639c added some comments about this ticket but I don't think that any commit explicitly addressed issues reported here.

comment:3 Changed 4 years ago by simonpj

It does not work in HEAD for me. I get

simonpj@cam-05-unx:~/tmp$ ~/5builds/HEAD-4/inplace/bin/ghc-stage1 -c -dcore-lint T10432.hs
RAE1
  [W] cobox_arV :: ka1_arO[sk] ~ kb1_arP[sk] (CNonCanonical)
  ka1_arO[sk]
  kb1_arP[sk]
  False

T10432.hs:17:15: error:
    Couldn't match kind ‘ka1’ with ‘kb1’
      ‘ka1’ is untouchable
        inside the constraints: 'WrapType a1 ~ 'WrapType b1
        bound by the type signature for:
                   foo :: ('WrapType a1 ~ 'WrapType b1) => r1
        at T10432.hs:17:15-46ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 7.11.20151006 for x86_64-unknown-linux):
	No skolem info: kb1_arP[sk]

for the code in comment:1

comment:4 Changed 4 years ago by jstolarek

I'm using a compiler built by ./validate from commit e2b579e8d77357e8b36f57d15daead101586ac8e and here's what I get for originally reported code:

[killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs
{-# LANGUAGE ExistentialQuantification, PolyKinds,
DataKinds, RankNTypes, GADTs, TypeOperators #-}
module T10432 where
import Data.Type.Equality

data WrappedType = forall a. WrapType a;

matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
  ('WrapType a :~: 'WrapType b) -> (('WrapType a ~ 'WrapType b) => r) -> r;
matchReflK Refl r = r;

[killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate-stage1 -c -dcore-lint T10432.hs

T10432.hs:8:15: error:
    Could not deduce: ka ~ kb
    from the context: 'WrapType a ~ 'WrapType b
      bound by the type signature for:
                 matchReflK :: ('WrapType a ~ 'WrapType b) => r
      at T10432.hs:(8,15)-(9,74)
    ‘ka’ is a rigid type variable bound by
         the type signature for:
           matchReflK :: 'WrapType a :~: 'WrapType b
                         -> (('WrapType a ~ 'WrapType b) => r) -> r
         at T10432.hs:8:15
    ‘kb’ is a rigid type variable bound by
         the type signature for:
           matchReflK :: 'WrapType a :~: 'WrapType b
                         -> (('WrapType a ~ 'WrapType b) => r) -> r
         at T10432.hs:8:15
    Expected type: 'WrapType b
      Actual type: 'WrapType a
    In the ambiguity check for the type signature for ‘matchReflK’:
      matchReflK :: forall (ka :: BOX) (kb :: BOX) (a :: ka) (b :: kb) r.
                    'WrapType a :~: 'WrapType b
                    -> (('WrapType a ~ 'WrapType b) => r) -> r
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘matchReflK’:
      matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
                    (WrapType a :~: WrapType b)
                    -> ((WrapType a ~ WrapType b) => r) -> r

And for the code in comment:1:

[killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs
{-# LANGUAGE ExistentialQuantification, PolyKinds,
DataKinds, RankNTypes, GADTs, TypeOperators #-}
module T10432 where
import Data.Type.Equality

data WrappedType = forall a. WrapType a;

matchReflK2 :: forall (a :: ka) (b :: kb) (r :: *).
              ('WrapType a :~: 'WrapType b) ->  r
matchReflK2 x
 = let foo :: ('WrapType a ~ 'WrapType b) => r
       foo = undefined
   in undefined

[killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate-stage1 -c -dcore-lint T10432.hs
[killy@xerxes : /dane/projekty/ghc/ghc-tests/types/T10432]

I have no idea why are we getting different behaviours :-/

comment:5 Changed 4 years ago by thomie

I can reproduce jstolarek's findings.

comment:6 Changed 4 years ago by jstolarek

Differential Rev(s): Phab:D1691

I tested again and now it seems that the code in original bug report as well as Simon's code in comment 1 are accepted. I added a regression test. Once it validates on Phab I think we can close this ticket.

comment:7 Changed 4 years ago by simonpj

Terrific, thanks. Yes, pls add regression and close.

comment:8 Changed 4 years ago by Jan Stolarek <jan.stolarek@…>

In f141f416/ghc:

Test #10432

Summary: A regression test for #10432, which seems to already be fixed.

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1691

GHC Trac Issues: #10432

comment:9 Changed 4 years ago by jstolarek

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T10432

comment:10 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.