Avoid `undefined` when using `TypeError` in type-class constraint-CodePudding

I have a type-class instance like this:

instance {-# OVERLAPPABLE #-} (TypeError ( 'Text "Some error")) => SomeClass x where
  someMethod = undefined

This instance exists at the end of other (valid) instances. The idea is to have the compiler throw a type error when the user writes a type that doesn't adhere to these valid instances. TypeError in instance constraint achieves this, but this also forces me to fill in the method with undefined, which feels like a hack.

Is there a way to avoid this? Or do it better?

Here's the real-world code with this pattern.

CodePudding user response：

The best I could achieve is this. Essentially, I defined a TypeErr type family standing for both the standard TypeError constraint and an additional Impossible constraint providing the needed witness. Impossible would always fail to resolve as a constraint, but the type error is triggered first anyway.

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

import GHC.TypeLits (
  ErrorMessage (Text),
  TypeError,
 )

class Impossible where
  impossible :: a

type family TypeErr t where
  TypeErr t = (TypeError t, Impossible)

-- Dummy example
class SomeClass x where
  someMethod :: x -> Maybe x

instance {-# OVERLAPPABLE #-} (TypeErr ( 'Text "Some error")) 
         => SomeClass x where
  someMethod = impossible

main :: IO ()
main = print (someMethod True)
{-
<source>:19:15: error:
    * Some error
    * In the first argument of `print', namely `(someMethod True)'
      In the expression: print (someMethod True)
      In an equation for `main': main = print (someMethod True)
-}

CodePudding user response：

We have the Disallowed class in the trivial-constraint package. It offers the nope pseudo-method, which is a version of undefined that can only be used in impossible contexts (and witnesses this by being possible to “use” unboxed, which you can't do with standard undefined).

instance {-# OVERLAPPABLE #-} (Disallowed "fallback for `SomeClass`")
    => SomeClass x where
  someMethod = nope