GitLab

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

  ið :: 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
>

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	mnguyen
Operating system
Architecture

b) (b (op_a -#- b)\r\ninstance Coercible (op_a --> b) (b (op_a -#- b)\r\n\r\nclass (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj\r\ninstance (forall (op_a :: obj) (b :: obj). op_a -#- b) => OpOpNoOp obj\r\n\r\nclass\r\n Ríki (obj :: Obj) where\r\n type (-->) :: obj -> obj -> Type\r\n\r\n ið :: a --> (a::obj)\r\n\r\nclass\r\n OpOpNoOp obj\r\n =>\r\n OpRíki (obj :: Obj) where\r\n type ( obj -> Type\r\n\r\ndata Op a = Op a\r\n\r\ntype family UnOp op where UnOp ('Op obj) = obj\r\n\r\nnewtype Y :: Cat (Op a) where\r\n Y :: (UnOp b --> UnOp a) -> Y a b\r\n\r\ninstance Ríki Type where\r\n type (-->) = (->)\r\n ið x = x\r\n\r\ninstance OpRíki (Op Type) where\r\n type (\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->