entail: involve (something) as a necessary or inevitable part or consequence: a situation which entails considerable risks.
entail: Check that the current set of type class dictionaries entail the specified type class goal, and, if so, return a type class dictionary reference.
So, it is typeclass related. It arguments:
moduleName : ModuleName: FIXME Where it is used?
context : M.Map (Maybe ModuleName) (M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) TypeClassDictionaryInScope))
- Too long name
- Basically a $module \mapsto (class \mapsto (ident \mapsto dictionary))$
(Qualified (ProperName 'ClassName), [Type])
So, "type class goal" is the constraint.
solve either solve it and return
Expr which is a plain–value form of type class.
work looks interesting to me. If
work is too large (>1000), a
PossiblyInfiniteInstance error will be triggered. Pay attention to
solveSubgoals, which creates dictionaries for subgoals which still need to be solved by calling go recursively. E.g. the goal
(Show a, Show b) => Show (Either a b) can be satisfied if the current type unifies with
Either a b, and we can satisfy the subgoals
Show a and
Show b recursively.
One point is the relationship between "super class" and "sub class".
TODO: Maybe I should read the original paper of Haskell to make context a little clearer.
overlapping's motivation: Dictionaries which are subclass dictionaries cannot overlap.
mkDictionary's branching is interesting: It is used with
args, which are returned value of
solveSubgoal, and later used as initial part of
solveSubgoalis passed with no constraints, dictionary value is local
- If empty
args, dictionary value is global
- If empty
args, dictionary value is dependent
So, can you tell me what does
Every type is checked to satisfy the constraint under the context. Type can be base type $\tau$ or constructed type $\kappa \, \tau$. For the base type, it is simply queried; For the constructed type, we will query its constructor. The constructor might be polymorphic. But the one with instance must be more polymorphic. Beyond that, the typeclass's superclass might bring other constraints, which should be solved.
typeHeadsAreEqual: What is "type heads"?
TypeConstructor are referred. Row constructor
RCons is also used. I think it wants to extract what would be used in type class declaration, i.e. the $\alpha$. The $\alpha$ can be parameterized.