Skip to content

Improve output of pattern synonym info

import GHC.Prim
import Data.Kind

data TypeRep :: forall k. k -> Type where
  TI :: TypeRep Int
  TB :: TypeRep Bool
  TL :: TypeRep []
  TA :: TypeRep f -> TypeRep x -> TypeRep (f x)

data (a::k1) :~~: (b::k2) where
  HRefl :: a :~~: a
deriving instance Show (a :~~: b)

eqTT :: TypeRep (a::k1) -> TypeRep (b::k2) -> Maybe (a :~~: b)
eqTT TI TI = Just HRefl
eqTT TB TB = Just HRefl
eqTT TL TL = Just HRefl

pattern IsList <- (eqTT TL -> Just HRefl)
  where IsList = TL

What is the type of IsList? The result of :type is only accurate when used as an expression (IsList :: TypeRep []) and the result of :info is uses ~#

>>> :info IsList
pattern IsList :: forall k2 (b :: k2). () => ((* -> *) ~# k2,
                                              [] ~# b) => TypeRep b

which won't parse (parse error on input ‘~#’).

-- t9R4.hs:20:67: error: …
--     • Expected kind ‘* -> *’, but ‘b’ has kind ‘k2’
--     • In the second argument of ‘~’, namely ‘b’
-- Compilation failed.
pattern IsList :: forall k2 (b :: k2). () => ((* -> *) ~ k2, [] ~ b) => TypeRep b
pattern IsList <- (eqTT TL -> Just HRefl)
  where IsList = TL

The user may try to use ~ but we need heterogeneous equality from GHC.Types (~~)

pattern IsList :: forall k2 (b :: k2). () => ((* -> *) ~ k2, [] ~~ b) => TypeRep b

and in the end, we only need

pattern IsList :: () => [] ~~ b => T b

:info should show something closer to that! Copy-pasting should work

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information