Changes that Break Backwards Compatibility

Although backwards compatibility is a good goal to aim for, sometimes it is not possible. This page documents when backwards compatibility has been broken, which versions of Idris were affected, and what the changes were.

Namespace Visibility

Prior to Idris 0.9.15.1 if a module B imports a module A, then a module C imports B, the public names in A would also be visible to C (i.e. B would automatically reexport everything from A). Commit https://github.com/idris-lang/Idris-dev/commit/7b5f4aa392985c6a7d7fdd5268cebe4adee954b8 changes the default behaviour so that the only names exported from a module are those defined in that module. If B imports A and wants to reexport everything in A, then A should be imported with the "public" modifier (i.e. "import public A").

Consistent Naming

Idris v0.9.14.3 introduced consistent naming accross the Idris prelude and base packages. These changes were discussed in Issue #1516, and fixed in PR #1553. Further renaming was done as part of Idris v0.9.15 which is described by PR #1619.

Prelude

Module name	Old Name	New Name
built in	refl	Refl
Builtins	_\|_	Void
Builtins	FalseElim	void
Builtins	Sg_Into	MkSigma
Bool	so	So
Bool	oh	Oh
Pairs	evidence	Evidence
Pairs	element	Element
Fin	fZ	FZ
Fin	fS	FS
Nat	lteZero	LTEZero
Nat	lteSucc	LTESucc
Nat	cmpLT	CmpLT
Nat	cmpEQ	CmpEQ
Nat	cmpGT	CmpGT