diff --git a/docs/users_guide/debug-info.rst b/docs/users_guide/debug-info.rst
index 8af2b5b60801089781a45b4254cc1728eb97c621..f82a4e48a5cc40ccf454e81dd130ef049b69f04d 100644
--- a/docs/users_guide/debug-info.rst
+++ b/docs/users_guide/debug-info.rst
@@ -251,7 +251,7 @@ Implementor's notes: DWARF annotations
interpret the GHC-specific DWARF annotations contained in compiled binaries.
When invoked with the ``-g`` flag GHC will produce standard `DWARF v4
-<http://dwarfstd.org/>`__ debugging information. This format is used by nearly
+<https://dwarfstd.org/>`__ debugging information. This format is used by nearly
all POSIX-compliant targets and can be used by debugging and performance tools
(e.g. ``gdb``, ``lldb``, and ``perf``) to understand the structure of
GHC-compiled programs.
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index 89ecf8473d3d9b43aa46ee9cf49970a777563556..9190178ec1a1215f8cecca38c8cbcbc6f494c51c 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -43,9 +43,9 @@ refinement*. For example, in the right hand side of the equation ::
the type ``a`` is refined to ``Int``. That's the whole point! A precise
specification of the type rules is beyond what this user manual aspires
to, but the design closely follows that described in the paper `Simple
-unification-based type inference for
-GADTs <https://research.microsoft.com/%7Esimonpj/papers/gadt/>`__, (ICFP
-2006). The general principle is this: *type refinement is only carried
+unification-based type inference for GADTs
+<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gadt-pldi.pdf>`__
+(ICFP 2006). The general principle is this: *type refinement is only carried
out based on user-supplied type annotations*. So if no type signature is
supplied for ``eval``, no type refinement happens, and lots of obscure
error messages will occur. However, the refinement is quite general. For
@@ -153,9 +153,9 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
A type is "rigid" if it is completely known to the compiler at its
binding site. The easiest way to ensure that a variable has a rigid type
is to give it a type signature. For more precise details see `Simple
- unification-based type inference for
- GADTs <https://research.microsoft.com/%7Esimonpj/papers/gadt/>`__. The
- criteria implemented by GHC are given in the Appendix.
+ unification-based type inference for GADTs
+ <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gadt-pldi.pdf>`__.
+ The criteria implemented by GHC are given in the Appendix.
- When GHC typechecks multiple patterns in a function clause, it typechecks
each pattern in order from left to right. This has consequences for patterns
diff --git a/docs/users_guide/exts/pragmas.rst b/docs/users_guide/exts/pragmas.rst
index aff9fc253a7e21d955c2f7f7de8f9c72042dfc14..6236df7beea0f2d311c1b8a022168128bbcd36db 100644
--- a/docs/users_guide/exts/pragmas.rst
+++ b/docs/users_guide/exts/pragmas.rst
@@ -365,7 +365,7 @@ has a number of other effects:
GHC ensures that inlining cannot go on forever: every mutually-recursive
group is cut by one or more *loop breakers* that is never inlined (see
`Secrets of the GHC inliner, JFP 12(4) July
-2002 <https://research.microsoft.com/%7Esimonpj/Papers/inlining/index.htm>`__).
+2002 <https://simonmar.github.io/bib/papers/inline.pdf>`__).
GHC tries not to select a function with an ``INLINE`` pragma as a loop
breaker, but when there is no choice even an INLINE function can be
selected, in which case the ``INLINE`` pragma is ignored. For example, for a
diff --git a/docs/users_guide/exts/type_families.rst b/docs/users_guide/exts/type_families.rst
index c185592bb55a4816f5e1637b9e43c22c00a7c6e7..7f9ecaa7ea637c75d4c5f56c492b0c77a8f5836f 100644
--- a/docs/users_guide/exts/type_families.rst
+++ b/docs/users_guide/exts/type_families.rst
@@ -51,7 +51,7 @@ families <https://www.haskell.org/haskellwiki/GHC/Indexed_types>`__.
.. [AssocDataTypes2005]
“`Associated Types with Class
- <http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html>`__\ â€, M.
+ <https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/assoc.pdf>`__\ â€, M.
Chakravarty, G. Keller, S. Peyton Jones,
and S. Marlow. In Proceedings of “The 32nd Annual
ACM SIGPLAN-SIGACT Symposium on Principles of
@@ -59,15 +59,15 @@ families <https://www.haskell.org/haskellwiki/GHC/Indexed_types>`__.
Press, 2005.
.. [AssocTypeSyn2005]
- “`Type Associated Type
- Synonyms <http://www.cse.unsw.edu.au/~chak/papers/CKP05.html>`__\ â€. M.
+ “`Associated Type Synonyms
+ <https://www.microsoft.com/en-us/research/wp-content/uploads/2005/01/at-syns.pdf>`__\ â€, M.
Chakravarty, G. Keller, and S. Peyton Jones. In Proceedings of “The
Tenth ACM SIGPLAN International Conference on Functional Programmingâ€,
ACM Press, pages 241-253, 2005.
.. [TypeFamilies2008]
- “\ `Type Checking with Open Type
- Functions <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html>`__\ â€,
+ “\ `Type Checking with Open Type Functions
+ <https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/icfp2008.pdf>`__\ â€,
T. Schrijvers, S. Peyton-Jones, M. Chakravarty, and M. Sulzmann, in
Proceedings of “ICFP 2008: The 13th ACM SIGPLAN International Conference
on Functional Programmingâ€, ACM Press, pages 51-62, 2008.
@@ -548,8 +548,8 @@ Decidability of type synonym instances
In order to guarantee that type inference in the presence of type
families is decidable, we need to place a number of additional restrictions
on the formation of type instance declarations (c.f., Definition 5
-(Relaxed Conditions) of “\ `Type Checking with Open Type
-Functions <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html>`__\ â€).
+(Relaxed Conditions) of “\ `Type Checking with Open Type Functions
+<https://www.microsoft.com/en-us/research/wp-content/uploads/2008/01/icfp2008.pdf>`__\ â€).
Instance declarations have the general form ::
type instance F t1 .. tn = t
@@ -1158,7 +1158,7 @@ will be possible to infer ``t`` at call sites from the type of the argument: ::
Injective type families are enabled with ``-XTypeFamilyDependencies`` language
extension. This extension implies ``-XTypeFamilies``.
-For full details on injective type families refer to Haskell Symposium
+For full details on injective type families refer to the Haskell Symposium
2015 paper `Injective type families for
Haskell <https://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones_eisenberg_injectivity_extended.pdf>`__.
diff --git a/docs/users_guide/exts/view_patterns.rst b/docs/users_guide/exts/view_patterns.rst
index d77a24cf53afa60df55f766a6f346d14c46705d9..99705fec3294ade236a3da7966fd1236b4292b75 100644
--- a/docs/users_guide/exts/view_patterns.rst
+++ b/docs/users_guide/exts/view_patterns.rst
@@ -119,8 +119,8 @@ follows:
into a single nested case expression, so that the view function is
only applied once. Pattern compilation in GHC follows the matrix
algorithm described in Chapter 4 of `The Implementation of Functional
- Programming
- Languages <https://research.microsoft.com/~simonpj/Papers/slpj-book-1987/>`__.
+ Programming Languages
+ <https://www.microsoft.com/en-us/research/wp-content/uploads/1987/01/slpj-book-1987-small.pdf>`__.
When the top rows of the first column of a matrix are all view
patterns with the "same" expression, these patterns are transformed
into a single nested case. This includes, for example, adjacent view