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 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 defaulting 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:
_s0 with a related constraint InferDoorState _s0._s0 := Any, but this requires no wanted constraints to mention _s0.InferDoorState _s0, and it fails. (Note that there being an InferDoorState s available does nothing to help, since it does not imply _s0 ~ s.)