haskellghctypeclasssingleton-type# GHC not deriving typeclass instances based on input type

I've lately been experimenting with dependent typing in Haskell through the Singletons library. To gain a better understanding I've been playing with my own implementations of various types without using the library. However, I've encountered issues getting the compiler to construct the right singleton members via type classes, and my first instinct fails to compile.

In particular, a tutorial that I've been following has these definitions (see https://blog.jle.im/entry/introduction-to-singletons-1.html):

```
data DoorState = Locked | Closed | Open deriving (Eq, Show)
newtype Door (s :: DoorState) = UnsafeMkDoor {doorMaterial :: String} deriving (Eq, Show)
```

With a singleton type family defined for each element of type `DoorState`

:

```
data SDoorState :: DoorState -> * where
SLocked :: SDoorState Locked
SClosed :: SDoorState Closed
SOpen :: SDoorState Open
```

And corresponding typeclasses for deriving singleton members automatically:

```
class InferDoorState s where
getSDoorState :: SDoorState s
instance InferDoorState 'Closed where
getSDoorState = SClosed
instance InferDoorState 'Locked where
getSDoorState = SLocked
instance InferDoorState 'Open where
getSDoorState = SOpen
```

For the below function, the version in the tutorial does compile, but I think I would've implemented it as below. The function is to turn a singleton type into a concrete element. This implementation (my first instinct) doesn't compile:

```
doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ _ = toDoorState getSDoorState -- ERROR!
-- ERROR: Could not deduce (InferDoorState s0)
-- arising from a use of ‘getSDoorState’
```

However, this does - if I manually specify the typeclass instance:

```
doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ (_ :: Door s) = toDoorState (getSDoorState @s)
```

It seems to me like the compiler should have been able to derive the associated typeclass instance based on the input type - but rather it doesn't use the constraint specified in the function for the input `Door s`

. I don't understand why this is.

Solution

The error is better described as the compiler not knowing what `DoorState`

you intend to call `getSDoorState`

at.

```
doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ _ = toDoorState (getSDoorState @_s0)
-- ERROR: don't know what _s0 should be set to!
```

After all, there's no technical reason the argument `_s0`

to `getSDoorState`

should be `s`

. `doorStatus_ _ = toDoorState (getSDoorState @Locked)`

might be stupid, but is type-correct nonetheless. As there is no unambiguous solution for `_s0`

, it is left unsolved, and you get an error. The complete GHC error I get when I compile your code *does* mention "The type variable `s0`

is ambiguous". That's the real error. (I'm marking unsolved holes with underscores, though GHC doesn't do so and also just calls them "type variables".)

The reason the error is buried under a "missing instance" type error is probably a consequence of the following GHC arcana. Consider the definition

```
-- under -XAllowAmbiguousTypes
test :: forall (s :: DoorState). Int
test = 4
```

You'll notice that something like `main = print test`

will compile, even though you think it should be interpreted as `main = print (test @_s0)`

, with an unsolvable `_s0`

hole. GHC is however willing to play the following dirty trick on you: if there is an unsolved type hole in the program, *and there are no unsolved constraints on that type either*, then the behavior of the program (by parametricity) actually can't depend on the type used to fill that hole. So GHC stuffs `GHC.Exts.Any`

into the hole to help the program get compiled. This is related to the `default`

ing process by which e.g. unsolved holes `_a`

where `Num _a`

is also wanted get defaulted by `_a := Integer`

.

```
type family Any :: k where -- "type-level 'undefined'", hence no instances
```

So, from GHC's perspective, the error in your program is discovered like this:

- GHC notices there is an unsolved type variable
`_s0`

with a related constraint`InferDoorState _s0`

. - This can be made okay only if GHC can default
`_s0 := Any`

, but this requires no wanted constraints to mention`_s0`

. - So GHC tries to solve
`InferDoorState _s0`

, and it fails. (Note that there being an`InferDoorState s`

available does nothing to help, since it does not imply`_s0 ~ s`

.) - An error is formulated where the failing step (3) is first in the error message but the underlying cause (1) is a little buried.

- Using pattern synonyms to abstract implementation of text type
- How to avoid listing A as build dependency for internal library/executable E just because E depends on internal library L which depends on A?
- How is the Foldable instance of (,) useful?
- What is the proper way of wrapping an Int (not a general type) in another type if type safety is the only motive?
- What is the most practical way to express a dependency on a library for which we have a local git repository with some changes?
- Htmx POST to haskell servant handling optional field in FormUrlEncoded request
- Haskell fails to infer the return type of a monad after using the sequence operator
- Does extracting values from a multiple Value return in Haskell invoke the function more than once?
- How to specify c/c++ compiler on stack install command
- Why do I get "Unexpected reply type" from notify-send when using this Haskell notification server?
- Don't understand notation of morphisms in Monoid definition
- Foldln in haskell
- Is this property of a functor stronger than a monad?
- How to Instantiate a Custom Data Type with Record Syntax and Multiple Constructors
- How do I make a minimal working example for the a DBus server?
- Is it safe to downgrade Haskell stack version?
- Haskell, list of natural number
- unfamiliar syntax in Haskell / Clash function type signature
- foldM with monad State does not type check
- Why does my Runge-Kutta implementation oscillate to 0?
- How do I get the desired behavior in my TCP server?
- Why does the Haskell PVP describe new functions as non-breaking?
- How do I correctly use toLower in Haskell?
- How can I write a notification server in Haskell?
- Every Lens' is a Traversal'... how?
- How do I crate a value of type a{sv} for a call to org.freedesktop.Notifications.Notify via DBus?
- Web Scraping With Haskell
- Double exclamation marks in Haskell
- Haskell Servant POST FormUrlEncoded for (Vector String) field
- Confusion about list types in Haskell