It doesn't achieve anything useful, and can be confusing because it
means behaviour is different for names where ambiguity is pruned by type
vs names where it isn't.
If a let binding doesn't elaborate with a 'precise' inference, revert to
generalising. I still don't like this - we really need to be able to
postpone choice of multiplicities during unification. But we can't, yet,
so here we go.
This is a little bit of a hack, but is for the situation where a case
block arises from the same bit of source but with a different name,
which would happen when elaborating interfaces with cases in a method
signature. If it's the same function with the same scrutinee, it's
convertible.
Fixes#191
This needed a bit of reorganisation, but it speeds up checking if a
module doesn't need rebuilding due to the import interfaces not
changing. Also it means that the "Type checking foo.idr" message is
displayed before parsing rather than after, which is probably better.
If we do, we might solve something we shouldn't because we're not
checking determining arguments. In 'defaults' mode, we should *only*
apply default hints - we'll go back to the locals in a final pass.
We've been generalising inferred function types to have multiplicity
RigW but sometimes (especially on lambdas) we need to infer the precise
type, so make a distinction.
This is pretty ugly, really. It would be better to be able to postpone
the choice until we know more, but it's not obvious to me how to achieve
that with the way unification is currently set up. The present way at
least works fine with code that doesn't use linearity, which is the
right default I think!
Now only abstracts over the environment once and deals with 'where'
clauses by rewriting the nested name with the rearranged environment. As
a result, it interacts far better with local definitions (i.e. where
blocks).
They're global, and so we don't reset per file, so we might get
duplicates, so it's much quicker to store as a map even though we'd
expect few of them overall.
Gets the OS info from the host compiler, which we'll need to be careful
with when bootstrapping (since maybe we'll distribute generated chez or
racket as a starting point for bootstrapping...)
Not in generating install directories, otherwise we end up with loads of
new directories for every patch and the purpose is to make it easy to
see which version you're working with.
The Chicken backend and reflection code are currently unused, and add to
memory usage and build time, so best leave them out for the moment.
They will be back! But probably best to wait until we can self host -
which hopefully won't be long - and we can take advantage of some of
the things Idris 2 does to compile quicker and using less space!
Always infer a multiplicity of W. Since we can pass a linear function to
one which expects an unrestricted argument, this gives the more general
result if the multiplicity is otherwise unknown.
This makes things like 'maybe id (+) x y' type check again even in the
presence of an 'id' which is declared linear!
This is the same as %auto_implicits in Idris 1, but with a more
appropriate name, because auto implicits are something else.
'%unbound_implicits off' turns off implicit forall bindings. See test
basic033 for an example.
In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
Need to use 'check' which expands ambiguous names, rather than
'checkImp' which does nothing. It won't insert any new dots since it
checks in expression context.
It's a big patch, but the summary is that it's okay to use a pattern in
an erased position if either:
- the pattern can also be solved by unification (this is the same as
'dot patterns' for matching on non-constructor forms)
- the argument position is detaggable w.r.t. non-erased arguments, which
means we can tell which pattern it is without pattern matching
The second case, in particular, means we can still pattern match on
proof terms which turn out to be irrelevant, especially Refl.
Fixes#178
