On 2021-10-30, Joachim Breitner
But the type checker also tries to preserves names, and in your example
Prelude> h (x : xs) = x Prelude> :t h h :: [a] -> a
I _think_ this is an `a` because the list type is declared roughtly like follows
data [a] = [] | a:[a]
Yes, Johannes also suggested that (though I missed it in my first reading of his message).
TyVarTv -> fsLit "a"
| TyVarTv -- A variant of TauTv, except that it should not be -- unified with a type, only with a type variable -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
The TyVarTv's which are named "a" appear, it says, only in kind signatures and partial type signatures, neither of which I understand, so presumably don't use.
And the others produce either t’s or p’s. For the "p", the relevant code is
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType newMetaTyVarTyAtLevel tc_lvl kind = do { details <- newTauTvDetailsAtLevel tc_lvl ; name <- newMetaTyVarName (fsLit "p") ; return (mkTyVarTy (mkTcTyVar name kind details)) }
but my knowledge of the type checker isn’t good enough to tell you in which situations this is used, and when to expect "p" and when to expect "t". And maybe GHC shouldn’t use "p" there, and simply consistently use "t", so that users aren’t even tempted to think about this…
Likewise, I can't work out what's going on here. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.