#12697 closed bug (duplicate)

Improve output of pattern synonym info

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.0.1
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12024 Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

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

Change History (3)

comment:1 Changed 12 months ago by simonpj

Thanks. Dup of #12024, which is awaiting #11660

comment:2 Changed 12 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 11 months ago by bgamari

Milestone: 8.2.1
Resolution: duplicate
Status: newclosed
Note: See TracTickets for help on using tickets.