Opened 11 months ago

Closed 8 months ago

Last modified 8 months ago

#15801 closed bug (fixed)

"ASSERT failed!" with visible kind applications

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.6.1
Keywords: TypeApplications Cc: mnguyen
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T15801
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5229
Wiki Page:

Description

Sorry for the workload mnguyen. This gives a very short error (using diff for visible kind application: https://phabricator.haskell.org/D5229)

{-# Language CPP                   #-}
{-# Language QuantifiedConstraints #-}
{-# Language TypeApplications      #-}
{-# Language PolyKinds             #-}
{-# Language TypeOperators         #-}
{-# Language DataKinds             #-}
{-# Language TypeFamilies          #-}
{-# Language TypeSynonymInstances  #-}
{-# Language FlexibleInstances     #-}
{-# Language GADTs                 #-}
{-# Language UndecidableInstances  #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleContexts      #-}

import Data.Coerce
import Data.Kind

type Cat ob = ob -> ob -> Type

type Obj = Type

class    Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)
instance Coercible (op_a --> b) (b <-- op_a) => (op_a -#- b)

class    (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj
instance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj

class
  Ríki (obj :: Obj) where
  type (-->) :: obj -> obj -> Type:: a --> (a::obj)

class
  OpOpNoOp obj
  =>
  OpRíki (obj :: Obj) where
  type (<--) :: obj -> obj -> Type

data Op a = Op a

type family UnOp op where UnOp ('Op obj) = obj

newtype Y :: Cat (Op a) where
  Y :: (UnOp b --> UnOp a) -> Y a b

instance Ríki Type where
 type (-->) = (->)
 ið x = x

instance OpRíki (Op Type) where
 type (<--) @(Op Type) = Y @Type
$ ghci -ignore-dot-ghci 577.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 577.hs, interpreted )
*** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line 1285
>

Change History (7)

comment:1 Changed 11 months ago by Iceland_jack

Can also be triggered with

>> :t coerce @(Y @Type _ _)
*** Exception: ASSERT failed! file compiler/typecheck/TcFlatten.hs, line 1285

comment:2 Changed 11 months ago by Richard Eisenberg <rae@…>

In 255d2e3/ghc:

Fix embarrassing, egregious bug in roles of (->)

Previously, I had inexplicably decided that (->)'s roles
were all Representational. But, of course, its first two
parameters are *dependent* RuntimeReps. All dependent parameters
have a Nominal role, because all roles in kinds are Nominal.

Fix is easy, but I have no idea how the world hasn't come
crashing down before now.

This was found while investigating #15801, which requires
visible type application in types to observe. Hence, the test
case will come with the main patch for #12045.

comment:3 Changed 10 months ago by RyanGlScott

I think a test case still needs to be added here?

comment:4 Changed 10 months ago by simonpj

Indeed it does. Richard says comment:2

Hence, the test case will come with the main patch for #12045.

comment:5 Changed 10 months ago by RyanGlScott

Urk, reading is hard for me today, apparently. Apologies for the noise.

comment:6 Changed 8 months ago by RyanGlScott

Differential Rev(s): Phab:D5229
Milestone: 8.8.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T15801

The test case (alluded to in comment:2) was added in 17bd163566153babbf51adaff8397f948ae363ca:

Author: mynguyen <mnguyen1@brynmawr.edu>
Date:   Tue Dec 18 11:52:26 2018 -0500

    Visible kind application
    
    Summary:
    This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
    It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
    written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
    application, just like in term-level.
    
    There are a few remaining issues with this patch, as documented in
    ticket #16082.
    
    Includes a submodule update for Haddock.
    
    Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a
    
    Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack
    
    Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter
    
    GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`
    
    Differential Revision: https://phabricator.haskell.org/D5229

comment:7 Changed 8 months ago by Richard Eisenberg <rae@…>

In 17bd1635/ghc:

Visible kind application

Summary:
This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
application, just like in term-level.

There are a few remaining issues with this patch, as documented in
ticket #16082.

Includes a submodule update for Haddock.

Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a

Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack

Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter

GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`

Differential Revision: https://phabricator.haskell.org/D5229
Note: See TracTickets for help on using tickets.