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.
The error is better described as the compiler not knowing what
DoorState
you intend to callgetSDoorState
at.After all, there's no technical reason the argument
_s0
togetSDoorState
should bes
.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 variables0
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
You'll notice that something like
main = print test
will compile, even though you think it should be interpreted asmain = 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 stuffsGHC.Exts.Any
into the hole to help the program get compiled. This is related to thedefault
ing process by which e.g. unsolved holes_a
whereNum _a
is also wanted get defaulted by_a := Integer
.So, from GHC's perspective, the error in your program is discovered like this:
_s0
with a related constraintInferDoorState _s0
._s0 := Any
, but this requires no wanted constraints to mention_s0
.InferDoorState _s0
, and it fails. (Note that there being anInferDoorState s
available does nothing to help, since it does not imply_s0 ~ s
.)