Unstable type expressions
Types can be passed around as firstclass values in several languages, either directly (particularly in languages with dependent types and universes) or as part of another structure (e.g. firstclass modules in OCaml, abstract type members in Scala).
This means that it is possible to have a type expression $T$ that depends on a value: if some boolean $b$ is false, then $T = \n{Int}$, but if it's true then $T = \n{String}$. In languages with mutation, there can even be a type expression $T$ where $T ≠ T$, because $T$ yields two different types when evaluated twice.
The risk is that if the type system does not perfectly track dependency of types on values, or the presence of sideeffects in type expressions, then you may end up with two incompatible values both claiming to be of type $T$.
The problem was noticed by Russo^{1}, in his thesis introducing firstclass modules to Standard ML, where he gave a counterexample showing that the naive approach was unsound. The issue later reappeared in Scala^{2}.
(* Counterexample by Claudio Russo *)
module F = functor (X:sig val b:bool end)
unpack
if X.b then
pack struct
type t = int
val x = 1
fun y n = n
end
as sig
type t
val x : t
val y : t > t
end
else
pack struct
type t = bool
val x = true
fun y b = if b then false else true
end
as sig
type t
val x : t
val y : t > t
end
end
as sig
type t
val x : t
val y : t → t
end
module A = F (struct val b = true end)
module B = F (struct val b = false end)
val z = A.y B.x
// Counterexample by Vladimir Reshetnikov
trait A {
type T
var v : T
}
object B {
def f(x : { val y : A }) { x.y.v = x.y.v }
var a : A = _
var b : Boolean = false
def y : A = {
if(b) {
a = new A { type T = Int; var v = 1 }
a
} else {
a = new A { type T = String; var v = "" }
b = true
a
}
}
}
// B.f(B) causes a ClassCastException
There are two standard fixes:

Syntactically restrict expressions appearing in types
The syntax of type expressions can be limited to constructions whose value cannot change. See paths in MLfamily languages and stable identifiers in Scala.
This can lead to some surprises, because valid syntax then depends on context. For instance, in OCaml, anonymous module parameters are possible in module definitions but not type expressions:
module X = struct type t = int end module FX = F (X) (* ok *) type t1 = (F (X)).t (* ok *) module FX = F (struct type t = int end) (* ok *) type t2 = (F (struct type t = int end)).t (* error *)
(Anonymous module parameters also cause other surprises: see the avoidance problem)

Restrict effects of expressions appearing in types
If the language statically tracks effects, either directly with a typeandeffect system or via encoding all effects in an
IO
monad, then it is possible to check that only pure expressions are used in types.There is an additional wrinkle here: some effect systems track mutation but allow nontermination to count as "pure". Depending on the exact system, allowing a possiblynonterminating expression into the type language may be unsound because of a typelevel version of the eventually, nothing problem.
Fig 7.12 on p. 270 of Types For Modules, Claudio Russo (1998)