Force index for group by is not always honored

drop table if exists t;

create table t(id int auto_increment, ts timestamp not null, primary key(id,ts)) engine=InnoDB, stats_sample_pages = 20;

insert into t(ts) values ('2017-01-01');

insert into t(ts) values ('2017-01-01');

replace into t(ts) select t1.ts from t t1, t t2, t t3, t t4, t t5, t t6, t t7, t t8, t t9, t t10, t t11, t t12, t t13, t t14, t t15;

insert into t(id,ts) select distinct id, '2017-01-02' from t;

select count(distinct id) from t;

analyze table t;

show indexes from t;

explain select id, max(ts) from t group by id;

explain select id, max(ts) from t force index for group by (primary) group by id;

{

  "query_block": {

{

  "query_block": {

    "select_id": 1,

    "r_loops": 1,

    "r_total_time_ms": 28.534,

    "table": {

      "table_name": "t",

      "access_type": "index",

      "key": "PRIMARY",

      "key_length": "8",

      "used_key_parts": ["id", "ts"],

      "r_loops": 1,

      "rows": 66792,

      "r_rows": 65540,

      "r_total_time_ms": 9.2646,

      "filtered": 100,

      "r_filtered": 100,

      "using_index": true

    }

  }

}