Opened 3 years ago

Last modified 3 years ago

#12048 new feature request

Allow CustomTypeErrors in type synonyms (+ evaluate nested type family?)

Reported by: Iceland_jack Owned by: diatchki
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: CustomTypeErrors Cc: RyanGlScott, jkarni
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

I didn't find a ticket with this, but with wiki:Proposal/CustomTypeErrors you can't define a type synonym without it erroring:

-- error: …
--     • onetwothree
--     • In the type synonym declaration for ‘ERROR’
-- Compilation failed.
type ERROR = TypeError (Text "onetwothree")

but I often want to factor out error messages, they are clunky to write at the type level and I often want to reuse message in many different type families, especially when they can be determined by a type family. Here's a hypothetical example:

type family
  Whoami (ty :: Type) :: Symbol where
  Whoami Int   = "a number"
  Whoami Float = "a number"
  Whoami [_]   = "a list of things"
  Whoami _     = "something else"

I would like to write

type Error ty = 
  TypeError (Text "Expected a <...> but got ":<>: Text (Whoami ty))

Even when ‘inlined’, it displays Expected a GRUE but got 'Text (Whoami Int) and not • Expected a GRUE but got a number.:

a :: TypeError (Text "Expected a GRUE but got ":<>: Text (Whoami Int))
a = 'a'

Change History (6)

comment:1 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 3 years ago by simonpj

Owner: set to diatchki

comment:3 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:4 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:5 Changed 3 years ago by jkarni

Cc: jkarni added

comment:6 Changed 3 years ago by andrewthad

Just to add information about my current workaround, the example given can be rewritten to use a type family instead:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Kind

-- Works just like a type synonym
type family Fail where
   Fail = TypeError (Text "It failed")

type family Bad a where
   Bad a = TypeError (Text "It messed up on " :<>: Text (Whoami a))

type family
  Whoami (ty :: Type) :: Symbol where
  Whoami Int   = "a number"
  Whoami Float = "a number"
  Whoami [_]   = "a list of things"
  Whoami _     = "something else"

expr :: Bad [Bool]
expr = 5

main :: IO ()
main = putStrLn "Hello"

Everyone on this ticket is probably already aware of this, but I just wanted to document it for passersby like myself who may be less familiar with the issue.

Note: See TracTickets for help on using tickets.