I am trying to understand the internal code of haskell-skiplist.
The author defines the following algebraic data type and some relevant functions – the details of which do not really matter.
data Node k v
= Node { nKey :: k
, nValue :: v
, nSibling :: Node k v
, nChild :: Node k v }
| Head { nSibling :: Node k v
, nChild :: Node k v }
| Nil
nodeLTKey :: forall k v. Ord k => Node k v -> k -> Bool
nodeEQKey :: forall k v. Eq k => Node k v -> k -> Bool
sibling :: forall k v. Node k v -> Node k v
Later in the insert function around line 113, they define a helper function of type Node k v -> (Node k v, Int). I have extracted the part I am confused about below.
go Nil = (Nil, wins)
go n
| nodeLTKey sN k = (n {nSibling = fst $ go sN}, -1)
| nodeEQKey sN k = (n {nSibling = sN {nValue = v}}, -1)
-- how can they update the inner record?
where
sN = sibling n
-- How can the compiler be sure that sN is a Node and not Head / Nil?
The sibling function returns a Node k v and only one of the possible variants of a Node k v actually has a field called nValue. I don't understand how the second guard can be sure that sN will have an nValue field – i.e that sN will be of the Node case and not Head / Nil.
From just the types and code posted, indeed there is no guarantee that sN will be of the Node constructor, and the code could fail at runtime. But if we look at context you linked but did not copy, nodeEQKey is defined to only return True for Node objects whose field matches nodeEQKey's parameter. So the second equation can safely update its nValue, because its body will only be executed if its guard matches, which will only happen if sN is a Node with nKey == k.
The compiler does not guarantee this node will have the right shape; the check happens at runtime. But if you turn on -Wall, you will be warned of an incomplete pattern match, which could fail at runtime.