diff --git a/lib/debugger/src/dbg_wx_view.erl b/lib/debugger/src/dbg_wx_view.erl
index 86d009238f8a..d4e21768ce84 100644
--- a/lib/debugger/src/dbg_wx_view.erl
+++ b/lib/debugger/src/dbg_wx_view.erl
@@ -55,6 +55,7 @@ stop() ->
 %% Main loop and message handling
 %%====================================================================
 
+-spec init(term(), term(), term(), term()) -> no_return().
 init(GS, Env, Mod, Title) ->
     wx:set_env(Env),
     %% Subscribe to messages from the interpreter
diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index 8e9b32434e3a..664ef479fe2e 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -1677,17 +1677,17 @@ bitstr_bitsize_type(Size) ->
       any
   end.
 
-%% Return the infimum (meet) of ExpectedType and Type if is not
-%% t_none(), and raise a bind_error() it is t_none().
+%% Return the infimum (meet) of ExpectedType and Type if it describes a
+%% possible value (not 'none' or 'unit'), otherwise raise a bind_error().
 bind_checked_inf(Pat, ExpectedType, Type, Opaques) ->
   Inf = t_inf(ExpectedType, Type, Opaques),
-  case t_is_none(Inf) of
+  case t_is_none_or_unit(Inf) of
     true ->
       case t_find_opaque_mismatch(ExpectedType, Type, Opaques) of
-        {ok, T1, T2}  ->
+        {ok, T1, T2} ->
           bind_error([Pat], T1, T2, opaque);
         error ->
-          bind_error([Pat], Type, t_none(), bind)
+          bind_error([Pat], Type, Inf, bind)
       end;
     false ->
       Inf
diff --git a/lib/dialyzer/test/user_SUITE_data/results/gh6580 b/lib/dialyzer/test/user_SUITE_data/results/gh6580
new file mode 100644
index 000000000000..6060365082ce
--- /dev/null
+++ b/lib/dialyzer/test/user_SUITE_data/results/gh6580
@@ -0,0 +1,7 @@
+
+gh6580.erl:11:21: The pattern <[_ | _], _> can never match the type <[],<<>>>
+gh6580.erl:5:1: Function f/0 has no local return
+gh6580.erl:6:5: The created fun has no local return
+gh6580.erl:6:5: The pattern <[], _> can never match the type <<<>>,<<>>>
+gh6580.erl:6:5: The pattern <[_ | _], _> can never match the type <<<>>,<<>>>
+gh6580.erl:9:13: Fun application with arguments (<<>>,<<>>) will never return since it differs in the 1st argument from the success typing arguments: ([],any())
diff --git a/lib/dialyzer/test/user_SUITE_data/src/gh6580.erl b/lib/dialyzer/test/user_SUITE_data/src/gh6580.erl
new file mode 100644
index 000000000000..282e36ed7913
--- /dev/null
+++ b/lib/dialyzer/test/user_SUITE_data/src/gh6580.erl
@@ -0,0 +1,15 @@
+-module(gh6580).
+-export([f/0]).
+
+%% GH-6580: dialyzer would crash when binding an impossible cons.
+f() ->
+    <<
+        0
+     || _ <-
+            case ok of
+                X ->
+                    <<0 || _ <- []>>
+            end,
+        X <- 0,
+        #{X := Y} <- 0
+    >>.
diff --git a/lib/reltool/src/reltool_app_win.erl b/lib/reltool/src/reltool_app_win.erl
index c84c1562ee25..a1d95c7e4b27 100644
--- a/lib/reltool/src/reltool_app_win.erl
+++ b/lib/reltool/src/reltool_app_win.erl
@@ -98,6 +98,7 @@ open_mod(Pid, ModName) ->
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %% Server
 
+-spec init(term(), term(), term(), term(), term()) -> no_return().
 init(Parent, WxEnv, Xref, C, AppName) ->
     try
 	do_init(Parent, WxEnv, Xref, C, AppName)
diff --git a/lib/stdlib/src/peer.erl b/lib/stdlib/src/peer.erl
index ecf33b139ba6..b4867c1bdf7c 100644
--- a/lib/stdlib/src/peer.erl
+++ b/lib/stdlib/src/peer.erl
@@ -926,6 +926,7 @@ start_orphan_supervision() ->
 
 -record(peer_sup_state, {parent, channel, in_sup_tree}).
 
+-spec init_supervision(term(), term()) -> no_return().
 init_supervision(Parent, InSupTree) ->
     try
         process_flag(priority, high),
@@ -1055,6 +1056,7 @@ origin_link(MRef, Origin) ->
             origin_link(MRef, Origin)
     end.
 
+-spec io_server() -> no_return().
 io_server() ->
    try
        process_flag(trap_exit, true),
@@ -1068,6 +1070,7 @@ io_server() ->
             erlang:halt(1)
     end.
 
+-spec tcp_init([term()], term()) -> no_return().
 tcp_init(IpList, Port) ->
     try
         Sock = loop_connect(IpList, Port),